Zulip Chat Archive

Stream: new members

Topic: my code is so egregious


Huỳnh Trần Khanh (Jun 01 2021 at 04:19):

any tips to make this code look less egregious

import data.list.basic
import data.list.sort

def adaptor : list   
| [] := 0
| (head::rest) := if rest = [] then head else min head (adaptor rest)

lemma aux3 (values values' : list ) (h : values ~ values') : adaptor values = adaptor values' := begin
  induction h with d hd he hf hg hh aw ajd jvkd akdls fks ala fvn wow vnd,
  simp,
  rw adaptor,
  rw adaptor,
  split_ifs,
  simp,
  rw h at hf,
  have := list.perm_nil.mp (hf.symm),
  exfalso,
  exact h_1 this,
  exfalso,
  rw h_1 at hf,
  have := list.perm_nil.mp hf,
  exact h this,
  rw hg,
  rw adaptor,
  rw adaptor,
  rw adaptor,
  rw adaptor,
  split_ifs,
  exfalso,
  exact h_1,
  have : hh :: ajd  list.nil := list.cons_ne_nil hh ajd,
  exfalso,
  exact this h,
  have : hh :: ajd  list.nil := list.cons_ne_nil hh ajd,
  exfalso,
  exact this h,
  exfalso,
  exact h_1,
  simp [min_comm],
  rw min_comm,
  rw min_assoc,
  rw min_comm (adaptor ajd) aw,
  simp [wow, vnd],
end

Scott Morrison (Jun 01 2021 at 04:20):

Absolute #1 suggestion --- learn to use braces to delimit subgoals!

Scott Morrison (Jun 01 2021 at 04:21):

Basically if ever a tactic results in multiple goals, the next line should start with a brace. (Exceptions only if the next line is swap or show to reorder the goals.)

Scott Morrison (Jun 01 2021 at 04:21):

After that, read the #style guide.

Scott Morrison (Jun 01 2021 at 04:22):

Put multiple rw on the same line using rw [a, b, c].

Scott Morrison (Jun 01 2021 at 04:22):

If a tactic introduces new hypotheses that you actually use, name them yourself instead of using the auto-generated names.

Scott Morrison (Jun 01 2021 at 04:23):

(all those comments are without even attempting to read the statement or proof. :-)

Scott Morrison (Jun 01 2021 at 04:25):

You should rarely be using rw adaptor where adaptor is an inductive definition. Instead, make sure you have proved the appropriate @[simp] lemma adaptor_nil : ... := rfl and @[simp] lemma adaptor_cons : ... := rfl lemmas. (Or use the @[simps] attribute to automatically generate them.)

Scott Morrison (Jun 01 2021 at 04:26):

Writing good @[simp] lemmas is essential for nearly every definition you write.

Scott Morrison (Jun 01 2021 at 04:26):

(You should always be hoping that the borings corners of your proof are by { intros, ext, simp, }, and when they are not, you should wonder if they could be.)

Scott Morrison (Jun 01 2021 at 04:36):

(Okay, maybe that it slightly overstating the case. But good @[ext] and @[simp] lemmas make life easier for everyone who comes afterwards, so are worth thinking about!)

Thomas Browning (Jun 01 2021 at 07:13):

From a more mathematical point of view, you might find it easier to leverage the existing lemma list.perm.foldr_eq. Here's my attempt at this approach:

import data.list.basic
import data.list.sort

def adaptor : list   
| [] := 0
| (head::rest) := if rest = [] then head else min head (adaptor rest)

def adaptor_aux : list   with_top  := λ l, (l.map coe).foldr () 

lemma adaptor_aux_cons_ne_top (a : ) (l : list ) : adaptor_aux (a :: l)   :=
λ hl, (with_top.coe_ne_top (inf_eq_top_iff.mp hl).1).elim

lemma adaptor_aux_eq_top (l : list ) : adaptor_aux l =   l = list.nil :=
λ hl, by { cases l, refl, exact (adaptor_aux_cons_ne_top _ _ hl).elim }, congr_arg adaptor_aux

lemma adaptor_eq_adaptor_aux (l : list ) : adaptor l = option.get_or_else (adaptor_aux l) (0 : ) :=
begin
  induction l with a l ih,
  { refl },
  { by_cases hl : l = list.nil,
    { rw hl,
      refl },
    { rw  with_top.coe_eq_coe,
      change (ite _ _ (_  _)) = some _,
      rw [option.get_or_else_of_ne_none (adaptor_aux_cons_ne_top a l), if_neg hl, ih, with_top.coe_inf],
      change _  some _ = _,
      rw [option.get_or_else_of_ne_none (mt (adaptor_aux_eq_top l).mp hl)],
      refl } },
end

lemma aux3_aux (l₁ l₂ : list ) (h : l₁ ~ l₂) : adaptor_aux l₁ = adaptor_aux l₂ :=
list.perm.foldr_eq inf_left_comm (list.perm.map coe h) 

lemma aux3 (l₁ l₂ : list ) (h : l₁ ~ l₂) : adaptor l₁ = adaptor l₂ :=
by rwa [adaptor_eq_adaptor_aux, adaptor_eq_adaptor_aux, aux3_aux]

Damiano Testa (Jun 01 2021 at 10:57):

For an approach closer to your initial version, you can also do this:

import data.list.basic
import data.list.sort

variables {α : Type*} [linear_order α] [has_zero α] {x : α}

def adaptor : list α  α
| [] := 0
| (head::rest) := if rest = [] then head else min head (adaptor rest)

namespace adaptor

lemma cons_eq_min :  {l : list α} (l0 : l  []), adaptor (x :: l) = min x (adaptor l)
| [] l0    := (l0 rfl).elim
| (h::t) _ := rfl

lemma cons_eq {l₁ l₂ : list α} (p₁ : l₁  []) (p₂ : l₂  []) (h : adaptor l₁ = adaptor l₂) :
  adaptor (x :: l₁) = adaptor (x :: l₂) :=
(cons_eq_min p₁).trans ((congr_arg _ h).trans (cons_eq_min p₂).symm)

lemma aux3 (l₁ l₂ : list α) (h : l₁ ~ l₂) : adaptor l₁ = adaptor l₂ :=
begin
  induction h with d hd _ hf hg _ _ g _ _ _ _ _ wow vnd; clear l₁ l₂,
  { refl },
  { cases hd with a l,
    { rw hf.symm.eq_nil },
    { refine cons_eq (l.cons_ne_nil a) _ hg,
      exact λ j, l.not_perm_nil_cons a (hf.trans (list.perm_nil.mpr j)).symm } },
  { cases g,
    { exact min_comm _ _ },
    { exact min_left_comm _ _ _ } },
  { exact wow.trans vnd }
end

end adaptor

Note that with this version you again have to walk around the weirdness of the definition of adaptor for [], but you do it "internally".


Last updated: Dec 20 2023 at 11:08 UTC