my code is so egregious

Stream: new members

[Huỳnh Trần Khanh]

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]

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

[Scott Morrison]

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]

After that, read the #style guide.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

(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]

(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]

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]

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".