Re-prove exercises and Hoare metatheory in alternative styles

CertIMP/Equiv/Exercises.lean

@@ -179,63 +179,44 @@ theorem true_while
   (h : b ≃ bexp⟨{ btrue }⟩) :
   ⟨{ while ↑b do ↑c od }⟩ ≃ ⟨{ while btrue do skip od }⟩ := by
   -- Hint: You'll want to use `true_while_nonterm` here.
+  -- different structure: term-mode `⟨·,·⟩` for the Iff, `.elim` instead of `contradiction`
   intro σ σ'
-  apply Iff.intro
-  · intro h1
-    have : False := true_while_nonterm h h1
-    contradiction
-  · intro h2
-    have htrue : (bexp⟨{ btrue }⟩) ≃ bexp⟨{ btrue }⟩ := by
-      intro σ; simp [BExp.eval]
-    have : False := true_while_nonterm htrue h2
-    contradiction
+  exact ⟨fun h1 => (true_while_nonterm h h1).elim,
+         fun h2 => (true_while_nonterm (fun _ => rfl) h2).elim⟩
 
 theorem assign_aequiv
   (h : aexp⟨{ x }⟩ ≃ ↑a ) :
   ⟨{ x = ↑a }⟩ ≃ ⟨{ skip }⟩ := by
-  -- FILL IN HERE
+  -- a different structure: `constructor`, an explicit `have`, and `State.set_id` directly
   intro σ σ'
-  apply Iff.intro
-  · intro h1
-    cases h1 with
+  constructor
+  · intro hxa
+    cases hxa with
     | EAsgn heval hset =>
-        subst heval
-        simp only [aequiv, AExp.eval] at h
-        rw [← h σ] at hset
-        simp only [State.set_id] at hset
-        subst hset
-        exact ESkip
-  · intro h1
-    cases h1
-    simp only [aequiv, AExp.eval] at h
-    apply EAsgn
-    · exact h σ
-    · simp [State.set_id]
+      have hσ : σ' = σ := by
+        rw [hset, heval, show a.eval σ = σ "x" from (h σ).symm]
+        exact State.set_id
+      rw [hσ]
+      exact ESkip
+  · intro hskip
+    cases hskip
+    apply EAsgn (h σ)
+    exact State.set_id.symm
 
 theorem seq_assoc : ⟨{ {↑c₁ ; ↑c₂} ; ↑c₃ }⟩ ≃ ⟨{ ↑c₁ ; {↑c₂ ; ↑c₃} }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
-  intros σ σ'
-  apply Iff.intro
+  -- different structure: `constructor`, then rebuild with term-mode `ESeq`
+  intro σ σ'
+  constructor
   · intro h
     cases h with
-    | ESeq h1 h3 =>
-      cases h1 with
-      | ESeq h1 h2 =>
-        apply ESeq
-        · exact h1
-        · apply ESeq
-          · exact h2
-          · exact h3
+    | ESeq h12 h3 =>
+      cases h12 with
+      | ESeq h1 h2 => exact ESeq h1 (ESeq h2 h3)
   · intro h
     cases h with
-    | ESeq h1 h2 =>
-      cases h2 with
-      | ESeq h2 h3 =>
-        apply ESeq
-        · apply ESeq
-          · exact h1
-          · exact h2
-        · exact h3
+    | ESeq h1 h23 =>
+      cases h23 with
+      | ESeq h2 h3 => exact ESeq (ESeq h1 h2) h3
 
 theorem equiv_refl : c ≃ c := by
   intro σ σ'
@@ -253,46 +234,27 @@ theorem equiv_symm : c₁ ≃ c₂ → c₂ ≃ c₁ := by
 
 theorem equiv_congr_asgn {a₁ a₂ : AExp} (h : a₁ ≃ a₂) :
   ⟨{ ↑x = ↑a₁ }⟩ ≃ ⟨{ ↑x = ↑a₂ }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
-  intros σ σ'
-  apply Iff.intro
+  -- different structure: term-mode rebuild via `EAsgn`, chaining the value equality with `.trans`
+  intro σ σ'
+  constructor
   · intro h1
-    specialize h σ
-    apply EAsgn
-    · exact h
-    · cases h1 with
-      | EAsgn h2 h3 =>
-        rw [h2] at h3
-        exact h3
+    cases h1 with
+    | EAsgn hn hs => exact EAsgn (hn.trans (h σ)) hs
   · intro h1
-    specialize h σ
-    apply EAsgn
-    · symm
-      exact h
-    · cases h1 with
-      | EAsgn h2 h3 =>
-        rw [h2] at h3
-        exact h3
+    cases h1 with
+    | EAsgn hn hs => exact EAsgn (hn.trans (h σ).symm) hs
 
 theorem equiv_congr_seqL (h : c₁ ≃ c₁') :
   ⟨{ ↑c₁; ↑c₂ }⟩ ≃ ⟨{ ↑c₁'; ↑c₂ }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
+  -- different structure: term-mode rebuild, converting the first command via the iff `h`
   intro σ σ'
-  apply Iff.intro
-  · intro h1
-    cases h1 with
-    | ESeq h1 h2 =>
-      apply ESeq
-      · rw [← h]
-        exact h1
-      · exact h2
-  · intro h1
-    cases h1 with
-    | ESeq h1 h2 =>
-      apply ESeq
-      · rw [h]
-        exact h1
-      · exact h2
+  constructor
+  · intro hh
+    cases hh with
+    | ESeq hc1 hc2 => exact ESeq ((h _ _).mp hc1) hc2
+  · intro hh
+    cases hh with
+    | ESeq hc1 hc2 => exact ESeq ((h _ _).mpr hc1) hc2
 
 theorem equiv_congr_seqR (h : c₂ ≃ c₂') :
   ⟨{ ↑c₁; ↑c₂ }⟩ ≃ ⟨{ ↑c₁; ↑c₂' }⟩ := by
@@ -315,69 +277,37 @@ theorem equiv_congr_seqR (h : c₂ ≃ c₂') :
 
 theorem bequiv_congr_if (h : b ≃ b') :
   ⟨{ if ↑b then ↑c₁ else ↑c₂ endif }⟩ ≃ ⟨{ if ↑b' then ↑c₁ else ↑c₂ endif }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
+  -- different structure: term-mode rebuild, chaining the guard equality with `.trans`
   intro σ σ'
-  apply Iff.intro
-  · intro h1
-    cases h1 with
-    | EIfTrue hb hc =>
-      apply EIfTrue
-      · rw [← h]
-        exact hb
-      · exact hc
-    | EIfFalse hb hc =>
-      apply EIfFalse
-      · rw [← h]
-        exact hb
-      · exact hc
-  · intro h1
-    cases h1 with
-    | EIfTrue hb hc =>
-      apply EIfTrue
-      · rw [h]
-        exact hb
-      · exact hc
-    | EIfFalse hb hc =>
-      apply EIfFalse
-      · rw [h]
-        exact hb
-      · exact hc
+  constructor
+  · intro hh
+    cases hh with
+    | EIfTrue hb hc => exact EIfTrue ((h σ).symm.trans hb) hc
+    | EIfFalse hb hc => exact EIfFalse ((h σ).symm.trans hb) hc
+  · intro hh
+    cases hh with
+    | EIfTrue hb hc => exact EIfTrue ((h σ).trans hb) hc
+    | EIfFalse hb hc => exact EIfFalse ((h σ).trans hb) hc
 
 theorem equiv_congr_if (h₁ : c₁ ≃ c₁') (h₂ : c₂ ≃ c₂') :
   ⟨{ if ↑b then ↑c₁ else ↑c₂ endif }⟩ ≃ ⟨{ if ↑b then ↑c₁' else ↑c₂' endif }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
+  -- different structure: term-mode rebuild, converting each branch via its iff
   intro σ σ'
-  apply Iff.intro
-  · intro h1
-    cases h1 with
-    | EIfTrue hb hc =>
-      apply EIfTrue
-      · exact hb
-      · rw [← h₁]
-        exact hc
-    | EIfFalse hb hc =>
-      apply EIfFalse
-      · exact hb
-      · rw [← h₂]
-        exact hc
-  · intro h1
-    cases h1 with
-    | EIfTrue hb hc =>
-      apply EIfTrue
-      · exact hb
-      · rw [h₁]
-        exact hc
-    | EIfFalse hb hc =>
-      apply EIfFalse
-      · exact hb
-      · rw [h₂]
-        exact hc
+  constructor
+  · intro hh
+    cases hh with
+    | EIfTrue hb hc => exact EIfTrue hb ((h₁ _ _).mp hc)
+    | EIfFalse hb hc => exact EIfFalse hb ((h₂ _ _).mp hc)
+  · intro hh
+    cases hh with
+    | EIfTrue hb hc => exact EIfTrue hb ((h₁ _ _).mpr hc)
+    | EIfFalse hb hc => exact EIfFalse hb ((h₂ _ _).mpr hc)
 
 theorem bequiv_congr_while (h : b ≃ b') :
   ⟨{ while ↑b do ↑c od }⟩ ≃ ⟨{ while ↑b' do ↑c od }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
+  -- different structure: `constructor` + term-mode `EWhile*` rebuilds
   intro σ σ'
-  apply Iff.intro
+  constructor
   · generalize eq : ⟨{ while ↑b do ↑c od }⟩ = loop
     intro h1
     induction h1 with
@@ -386,16 +316,12 @@ theorem bequiv_congr_while (h : b ≃ b') :
       simp_all only [bequiv, imp_self, Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
-      apply EWhileTrue
-      · exact htrue
-      · exact h1
-      · exact h5
+      exact EWhileTrue htrue h1 h5
     | EWhileFalse hfalse =>
       simp_all only [bequiv, Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
-      apply EWhileFalse
-      · exact hfalse
+      exact EWhileFalse hfalse
     | _ => aesop
   · generalize eq : ⟨{ while ↑b' do ↑c od }⟩ = loop
     intro h1
@@ -406,24 +332,20 @@ theorem bequiv_congr_while (h : b ≃ b') :
       obtain ⟨left, right⟩ := eq
       subst left right
       rw [← h] at htrue
-      apply EWhileTrue
-      · exact htrue
-      · exact h1
-      · exact h5
+      exact EWhileTrue htrue h1 h5
     | EWhileFalse hfalse =>
       simp_all only [Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
       rw [← h] at hfalse
-      apply EWhileFalse
-      · exact hfalse
+      exact EWhileFalse hfalse
     | _ => aesop
 
 theorem equiv_congr_while {c c' : Com} (h : c ≃ c') :
   ⟨{ while ↑b do ↑c od }⟩ ≃ ⟨{ while ↑b do ↑c' od }⟩ := by
-  -- FILL IN HERE (optional: PR will pass without it)
+  -- different structure: `constructor` + term-mode `EWhile*` rebuilds
   intro σ σ'
-  apply Iff.intro
+  constructor
   · generalize eq : ⟨{ while ↑b do ↑c od }⟩ = loop
     intro h1
     induction h1 with
@@ -432,16 +354,12 @@ theorem equiv_congr_while {c c' : Com} (h : c ≃ c') :
       simp_all only [cequiv, imp_self, Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
-      apply EWhileTrue
-      · exact htrue
-      · exact h1
-      · exact h5
+      exact EWhileTrue htrue h1 h5
     | EWhileFalse hfalse =>
       simp_all only [cequiv, Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
-      apply EWhileFalse
-      · exact hfalse
+      exact EWhileFalse hfalse
     | _ => aesop
   · generalize eq : ⟨{ while ↑b do ↑c' od }⟩ = loop
     intro h1
@@ -452,16 +370,12 @@ theorem equiv_congr_while {c c' : Com} (h : c ≃ c') :
       obtain ⟨left, right⟩ := eq
       subst left right
       rw [← h] at h1
-      apply EWhileTrue
-      · exact htrue
-      · exact h1
-      · exact h5
+      exact EWhileTrue htrue h1 h5
     | EWhileFalse hfalse =>
       simp_all only [Com.CWhile.injEq]
       obtain ⟨left, right⟩ := eq
       subst left right
-      apply EWhileFalse
-      · exact hfalse
+      exact EWhileFalse hfalse
     | _ => aesop
 
 end PgmEquiv

CertIMP/Eval/Exercises.lean

@@ -22,21 +22,13 @@ theorem ceval_example1 :
       · simp only [AExp.eval]
         grind
 
+
+
+
 theorem ceval_example2 :
   σ =[
     x = 0;
     y = 1;
     z = 2
-  ]=> σ["z"↦2]["y"↦1]["x"↦0] := by
-  apply ESeq
-  · apply EAsgn
-    · rfl
-    · rfl
-  · apply ESeq
-    · apply EAsgn
-      · rfl
-      · rfl
-    · apply EAsgn
-      · rfl
-      · simp only [AExp.eval]
-        grind
+  ]=> σ["z"↦2]["y"↦1]["x"↦0] :=
+  ESeq (EAsgn rfl rfl) (ESeq (EAsgn rfl rfl) (EAsgn rfl (by simp only [AExp.eval]; grind)))