max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup proof

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-28 14:58:02 -07:00
parent 2a37f53fca
commit 5ca9b49235
1 changed files with 17 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
doc/examples/tc.lean
View file

@ -74,8 +74,12 @@ def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} :=
| .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂)
| _, _ => .unknown
theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .unknown) : e.typeCheck = .found ty h := by
revert h₂
cases typeCheck e with
| found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl
| unknown => intros; contradiction
-- TODO: for simplifying the following proof we need: ematching for forward reasoning, and `match` blast for case analysis
/-|
Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
@ -87,21 +91,19 @@ the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by
induction e with simp [typeCheck]
| plus a b iha ihb =>
revert iha ihb
cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
rename_i ty₁ _ ty₂ _ h _ _
cases ty₁ <;> cases ty₂ <;> simp at h
· have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
· have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
· have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
split
next => intros; contradiction
next ra rb hnp => -- Recall that hnp is a hypothesis generated by the `split` tactic that asserts the previous case was not taken
intro h ht
cases ht with
| plus h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
| and a b iha ihb =>
revert iha ihb
cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
rename_i ty₁ _ ty₂ _ h _ _
cases ty₁ <;> cases ty₂ <;> simp at h
· have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
· have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
· have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
split
next => intros; contradiction
next ra rb hnp =>
intro h ht
cases ht with
| and h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
/-|
Finally, we show that type checking for `e` can be decided using `Expr.typeCheck`.