From 5ca9b4923584da2c455c44d7c63a02c42364ef4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Mar 2022 14:58:02 -0700
Subject: [PATCH] chore: cleanup proof

---
 doc/examples/tc.lean | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/doc/examples/tc.lean b/doc/examples/tc.lean
index e4fd774fa5..766a020ca2 100644
--- a/doc/examples/tc.lean
+++ b/doc/examples/tc.lean
@@ -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`.