equality of decide

Stream: lean4

[Hannah Santos]

I've been trying to close this theorem for a while now, but it ends up on something I just don't know how to do anything about, really. The problem is if I can close this theorem with the goal I have now: decide (x + n ≤ y + n) = decide (x ≤ y), or if there might be something different that I could have done on my definitions or on the theorem itself.

inductive ListNat where
  | nil
  | cons : Nat → ListNat → ListNat
  deriving Repr

open ListNat
open Nat

def length : ListNat → Nat
  | nil => 0
  | cons _ l => length l + 1

def isSorted : ListNat → Bool
  | cons n (cons m l) => n ≤ m && isSorted (cons m l)
  | _ => true

def addNat : Nat → ListNat → ListNat
  | _, nil => nil
  | n, cons x xs => cons (x + n) (addNat n xs)

-- Useful theorems
theorem false_not_true :
  false ≠ true :=
by
  intro H
  cases H

theorem length_matters {l l' : ListNat} :
  l = l' → length l = length l' :=
by
  intro h
  rw [h]

axiom succ_inj {a b : Nat} : (succ a = succ b) → a = b
theorem not_eq_Add {n m : Nat} :
  m ≠ 0 → ¬ n = n + m :=
by
  intro h h'
  induction n with
  | zero =>
    rw [Nat.zero_add] at h'
    exact h h'.symm
  | succ n' H =>
    rw [Nat.succ_add] at h'
    exact H (succ_inj h')

theorem cons_one_neq_cons_more {x n m : Nat} {l : ListNat} :
  ¬ cons x nil = cons n (cons m l) :=
by
  intro h
  have lh: (length (cons x nil) = length (cons n (cons m l))) := length_matters h
  rw [length, length, length, length, Nat.zero_add, Nat.add_comm, Nat.add_succ (length l), Nat.add_zero] at lh
  exact not_eq_Add (Nat.succ_ne_zero (length l)) lh

theorem addNat_zero (l : ListNat) :
  addNat zero l = l :=
by
  induction l with
  | nil => rw [addNat]
  | cons x xs h => rw [addNat, Nat.add_zero, h]

theorem isSorted_addNat (n : Nat) (l : ListNat) :
  isSorted (addNat n l) = isSorted l :=
by-- Preciso de 2 casos base.
  induction l with
  | nil => rw [addNat]
  | cons x xs hyp =>
    cases xs with
    | nil =>
      rw [addNat, addNat, isSorted, isSorted]
      intro n m l' h
      exact cons_one_neq_cons_more h
      intro x y l' h'
      exact cons_one_neq_cons_more h'
    | cons y ys =>
      rw [addNat] at hyp
      rw [addNat, addNat, isSorted, hyp, isSorted]
      cases isSorted (cons y ys)
      rw [Bool.and_false, Bool.and_false]
      rw [Bool.and_true, Bool.and_true]

  /-1 goal
  case cons.cons.true
  nxy: Nat
  ys: ListNat
  hyp: isSorted (cons (y + n) (addNat n ys)) = isSorted (cons y ys)
  ⊢ decide (x + n ≤ y + n) = decide (x ≤ y)
  -/

[Alex J. Best]

I think you need some more lemmas, docs#decide_congr is the most important one. Are you trying to avoid using mathlib / std?
You can still copy paste some useful lemmas from them even if you don't want to import anything, eg.

inductive ListNat where
  | nil
  | cons : Nat → ListNat → ListNat
  deriving Repr

open ListNat
open Nat

def length : ListNat → Nat
  | nil => 0
  | cons _ l => length l + 1

def isSorted : ListNat → Bool
  | cons n (cons m l) => n ≤ m && isSorted (cons m l)
  | _ => true

def addNat : Nat → ListNat → ListNat
  | _, nil => nil
  | n, cons x xs => cons (x + n) (addNat n xs)

-- Useful theorems
theorem false_not_true :
  false ≠ true :=
by
  intro H
  cases H

theorem length_matters {l l' : ListNat} :
  l = l' → length l = length l' :=
by
  intro h
  rw [h]

axiom succ_inj {a b : Nat} : (succ a = succ b) → a = b
theorem not_eq_Add {n m : Nat} :
  m ≠ 0 → ¬ n = n + m :=
by
  intro h h'
  induction n with
  | zero =>
    rw [Nat.zero_add] at h'
    exact h h'.symm
  | succ n' H =>
    rw [Nat.succ_add] at h'
    exact H (succ_inj h')

theorem cons_one_neq_cons_more {x n m : Nat} {l : ListNat} :
  ¬ cons x nil = cons n (cons m l) :=
by
  intro h
  have lh: (length (cons x nil) = length (cons n (cons m l))) := length_matters h
  rw [length, length, length, length, Nat.zero_add, Nat.add_comm, Nat.add_succ (length l), Nat.add_zero] at lh
  exact not_eq_Add (Nat.succ_ne_zero (length l)) lh

theorem addNat_zero (l : ListNat) :
  addNat zero l = l :=
by
  induction l with
  | nil => rw [addNat]
  | cons x xs h => rw [addNat, Nat.add_zero, h]

theorem addNat_nil (l : ListNat) :
  addNat n nil = nil :=
  rfl

theorem addNat_cons (l : ListNat) :
  addNat n (cons m l) = cons (m + n) (addNat n l) :=
  rfl

theorem not_congr (h : a ↔ b) : ¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩
theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp

theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
  (decide_iff p).2

theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
  (decide_iff p).1

theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> exact by decide

theorem bool_eq_false {b : Bool} : ¬b → b = false :=
  bool_iff_false.1

theorem decide_false_iff (p : Prop) [Decidable p] : decide p = false ↔ ¬p :=
  bool_iff_false.symm.trans (not_congr (decide_iff _))
theorem of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p :=
  (decide_false_iff p).1

theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
  (decide_false_iff p).2
theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) :
    decide p = decide q := by
  cases h' : decide q with
  | false => exact decide_false (mt h.1 <| of_decide_false h')
  | true => exact decide_true (h.2 <| of_decide_true h')

theorem isSorted_cons : isSorted (cons n (cons m l)) = (n ≤ m && isSorted (cons m l)) := rfl
theorem add_le_add_iff {a b n : Nat}  : a + n ≤ b + n ↔ a ≤ b := sorry
theorem isSorted_addNat (n : Nat) (l : ListNat) :
  isSorted (addNat n l) = isSorted l :=
by-- Preciso de 2 casos base.
  induction l with
  | nil => rw [addNat]
  | cons x xs hyp =>
    rw [addNat_cons]
    cases xs with
    | nil =>
      rw [addNat, isSorted, isSorted]
      intro n m l' h
      exact cons_one_neq_cons_more h
      intro x y l' h'
      exact cons_one_neq_cons_more h'
    | cons y ys =>
      rw [addNat] at hyp
      rw [addNat_cons, isSorted_cons, hyp, isSorted_cons]
      rw [decide_congr add_le_add_iff]

[Hannah Santos]

Thank you, I'll try using that.