Skip to content

Instantly share code, notes, and snippets.

@JamesGallicchio
Created May 22, 2021 20:17
Show Gist options
  • Save JamesGallicchio/87e40a3fbd0b4c7ab3c1063f558517ad to your computer and use it in GitHub Desktop.
Save JamesGallicchio/87e40a3fbd0b4c7ab3c1063f558517ad to your computer and use it in GitHub Desktop.
structure mystruct := {a : ℕ} {b : ℕ}
def a_pred (s : mystruct) : option ℕ
:= match s.a with nat.zero := none
| (nat.succ a) := some a end
lemma mylemma
: ∀ {a' b : ℕ}, a_pred {a := a'.succ, b := b} = some a'
:= begin intros, simp [a_pred] end
theorem mytheorem
: ∀ {a b : ℕ}, a_pred {a := a, b := b}
= ite (a = a.pred) (none) (some a.pred)
:= begin
intros,
cases h : a,
simp [a_pred],
sorry
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment