From 0284be5c9b25275d1e8cd00c5f27aa6770c79def Mon Sep 17 00:00:00 2001 From: Stefan-Ivan <–i.stefann19@gmail.com> Date: Tue, 2 Jun 2026 11:12:19 +0300 Subject: [PATCH 1/2] exercises: Re-prove marked exercises in alternative styles Reworked all FILL-IN exercises + StackMachine lemmas with different proof structures (term-mode, constructor, congruence-lemma reuse). Full project builds (853 jobs). --- CertIMP/Equiv/Exercises.lean | 230 ++++++++------------------ CertIMP/Eval/Exercises.lean | 18 +- CertIMP/StackMachine/Lemmas.lean | 122 +++++++------- CertIMP/Transformation/Exercises.lean | 54 +----- 4 files changed, 141 insertions(+), 283 deletions(-) diff --git a/CertIMP/Equiv/Exercises.lean b/CertIMP/Equiv/Exercises.lean index 54cebf2..ff01efd 100644 --- a/CertIMP/Equiv/Exercises.lean +++ b/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 diff --git a/CertIMP/Eval/Exercises.lean b/CertIMP/Eval/Exercises.lean index 0fde743..66c2e50 100644 --- a/CertIMP/Eval/Exercises.lean +++ b/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))) diff --git a/CertIMP/StackMachine/Lemmas.lean b/CertIMP/StackMachine/Lemmas.lean index cb353b0..74b6b0a 100644 --- a/CertIMP/StackMachine/Lemmas.lean +++ b/CertIMP/StackMachine/Lemmas.lean @@ -16,97 +16,88 @@ attribute [local simp] stackPeek2 attribute [local simp] stackPeek1 lemma isErrorLemma {err st'} : ¬ Reachable (.error err) st' := by - intros h - generalize eq : (Except.error err) = st at h + -- different structure: discharge the `step` case with `simp at eq`, reuse the IH directly + intro h + generalize eq : (Except.error err : ExecutionState) = st at h induction h with - | step h => cases eq - | trans s1 s2 ih1 ih2 => - cases eq - simp only [imp_false, not_true_eq_false] at ih1 + | step _ => simp at eq + | trans _ _ ih1 _ => exact ih1 eq lemma isOOFLemma {st} : ¬ Reachable st (.error .OutOfFuel) := by - intros h - generalize eq : (Except.error ExecutionException.OutOfFuel) = st' at h + -- different structure: `subst` in the step case, reuse the IH directly in `trans` + intro h + generalize eq : (Except.error ExecutionException.OutOfFuel : ExecutionState) = st' at h induction h with - | @step μ _ h => - cases eq - simp [step, Bind.bind, Except.bind] at h + | @step μ _ hstep => + subst eq + simp [step, Bind.bind, Except.bind] at hstep aesop - | trans s1 s2 ih1 ih2 => - cases eq - simp only [imp_false, not_true_eq_false] at ih2 + | trans _ _ _ ih2 => exact ih2 eq lemma isFinalStepLemma {μ st} (h : isFinal (.ok μ)) : step μ = st → isError st := by + -- different structure: `subst` the step result first, then compute that `step` errors out + intro hstep + subst hstep rw [isFinal] at h - simp only [step, bind, Except.bind, fetchInstr, h, Nat.lt_irrefl, ↓reduceDIte] - intro h1 - rw [←h1, isError] - trivial + simp [step, bind, Except.bind, fetchInstr, h, isError] lemma isFinalLemma {st st'} (h : isFinal st) : Reachable st st' → isError st' := by - intro h - induction h with - | @step μ st'' hx => - exact isFinalStepLemma h hx - | @trans _ stx st'' s1 s2 ih1 ih2 => - apply ih1 at h + -- different structure: name the IH result, then case on the intermediate state + intro hr + induction hr with + | @step μ st'' hx => exact isFinalStepLemma h hx + | @trans _ _ st'' _ s2 ih1 _ => + have herr := ih1 h cases st'' with - | ok => contradiction - | error e => - have := @isErrorLemma e stx - contradiction + | ok => simp [isError] at herr + | error e => exact absurd s2 isErrorLemma lemma executeFinal {μ st fuel} (h : isFinal (.ok μ)) : execute fuel μ = st → st = .ok μ := by + -- different structure: `subst` the result, then unfold `execute` once intro h1 - rw [execute.eq_def] at h1 - simp [h] at h1 - symm - assumption + subst h1 + rw [execute.eq_def] + simp [h] lemma executeExtend {μ μ' fuel} (h : step μ = .ok μ') : execute (fuel + 1) μ = execute fuel μ' := by - rw [execute] - by_cases hx : μ.pc < μ.code.length - · rw [h] - by_cases hf : isFinal (Except.ok μ) - · rw [isFinal] at hf - aesop - · simp [hf] - · simp [step, hx, Bind.bind, Except.bind] at h + -- different structure: a successful step means μ is not final, so unfold `execute` once + have hnf : ¬ isFinal (.ok μ) := fun hf => by + have he := isFinalStepLemma hf h + simp [isError] at he + conv_lhs => rw [execute.eq_def] + rw [if_neg hnf, h] lemma executeStepFinal {μ st} (h1 : isFinal st) (h2 : step μ = st) : execute 1 μ = st := by - rw [execute] - by_cases hx : μ.pc < μ.code.length - · have hf : ¬ isFinal (Except.ok μ) := by - rw [isFinal] - intro habs - rw [habs] at hx - exact Nat.lt_irrefl μ.code.length hx - rw [h2] - simp only [hf, ↓reduceIte] - cases st with - | ok μ' => - simp only [execute, ite_eq_left_iff, reduceCtorEq, imp_false, Decidable.not_not] - exact h1 - | error => contradiction - · simp only [step, bind, Except.bind, fetchInstr, hx, ↓reduceDIte] at h2 - rw [←h2] at h1 - contradiction + -- different structure: derive not-final from h1+h2, then unfold `execute 1` then `execute 0` + have hnf : ¬ isFinal (.ok μ) := by + intro hf + have hi := isFinalStepLemma hf h2 + cases st with + | ok => simp [isError] at hi + | error => simp [isFinal] at h1 + conv_lhs => rw [execute.eq_def] + rw [if_neg hnf, h2] + cases st with + | ok μ' => + change execute 0 μ' = .ok μ' + rw [execute.eq_def, if_pos h1] + | error e => simp [isFinal] at h1 lemma executeLemmaAux {n : Nat} {μ μ' : MachineState} (h : Reachable (.ok μ) (.ok μ')) : ∃m, execute m μ = execute n μ' := by generalize eq1 : Except.ok μ = st at h generalize eq2 : Except.ok μ' = st' at h induction h generalizing n μ μ' with + -- different structure: term-mode witnesses (`⟨·,·⟩`) and `▸` for the final chain | step hs => cases eq1 cases eq2 - use n + 1 - exact executeExtend hs + exact ⟨n + 1, executeExtend hs⟩ | @trans _ _ sti _ _ ih1 ih2 => cases eq1 cases eq2 @@ -120,17 +111,16 @@ lemma executeLemmaAux {n : Nat} {μ μ' : MachineState} (h : Reachable (.ok μ) obtain ⟨m2, hm2⟩ := ih2 specialize @ih1 m2 μ μi rfl rfl obtain ⟨m1, hm1⟩ := ih1 - rw [hm2] at hm1 - use m1 + exact ⟨m1, hm2 ▸ hm1⟩ /-- Hard exercise, you will likely need the lemmas above, and possibly additional intermediary results. -/ lemma executeLemma {μ st} (h1 : Reachable (.ok μ) st) (h2 : isFinal st) : ∃ fuel : ℕ, execute fuel μ = st := by + -- different structure: case on st, reuse executeLemmaAux at fuel 0, term-mode witness cases st with - | error => contradiction + | error e => simp [isFinal] at h2 | ok μx => - obtain ⟨m, hm⟩ := @executeLemmaAux 0 _ _ h1 - use m - rw [hm, execute] - simp [h2] + obtain ⟨m, hm⟩ := executeLemmaAux (n := 0) h1 + refine ⟨m, ?_⟩ + rw [hm, execute.eq_def, if_pos h2] diff --git a/CertIMP/Transformation/Exercises.lean b/CertIMP/Transformation/Exercises.lean index 2a9edb0..9c23d3c 100644 --- a/CertIMP/Transformation/Exercises.lean +++ b/CertIMP/Transformation/Exercises.lean @@ -124,52 +124,14 @@ theorem fold_constants_com_sound : Com.fold_constants.sound := by | CWhile b c ih => -- FILL IN HERE -- (hint: think about the lemmas you proved previously about `while` commands) - apply Iff.intro - · intro h - unfold Com.fold_constants - cases h - · next h₁ => - split - · next habs => - rw [fold_constants_bexp_sound, habs, BExp.eval] at h₁ - contradiction - · apply ESkip - · apply EWhileFalse - rw [←fold_constants_bexp_sound] - exact h₁ - · next h₁ _ _ => - split - · next h' _ heq => - apply EWhileTrue _ ESkip - · exfalso - apply true_while_nonterm _ h' - intro - rw [fold_constants_bexp_sound, heq] - · simp only [BExp.eval] - · next habs => - rw [fold_constants_bexp_sound, habs, BExp.eval] at h₁ - contradiction - · next h' h'' _ _ _ => - apply EWhileTrue _ h' - · rw [←bequiv_congr_while (fold_constants_bexp_sound _)] - exact h'' - · rw [←fold_constants_bexp_sound, h₁] - · intro h - unfold Com.fold_constants at h - split at h - · next heq => - exfalso - apply true_while_nonterm _ h - rw [← heq] - aesop - · next heq => - cases h - rw [bequiv_congr_while (fold_constants_bexp_sound _), heq] - rw [false_while] - · exact ESkip - · aesop - · rw [bequiv_congr_while (fold_constants_bexp_sound _)] - exact h + -- different (and much shorter) structure: the guard folds to `b.fold_constants`, + -- and `b ≃ b.fold_constants`, so each branch is exactly one of our `while` lemmas. + have hb := fold_constants_bexp_sound b + unfold Com.fold_constants + cases hbf : b.fold_constants with + | BTrue => rw [hbf] at hb; exact true_while hb _ _ + | BFalse => rw [hbf] at hb; exact false_while hb _ _ + | _ => rw [hbf] at hb; exact bequiv_congr_while hb _ _ /- From 4bdb115df1d59e73ab2ba8147d28fd99f5f7e0b9 Mon Sep 17 00:00:00 2001 From: Stefan-Ivan <–i.stefann19@gmail.com> Date: Tue, 2 Jun 2026 16:21:17 +0300 Subject: [PATCH 2/2] hoare: Re-prove Hoare metatheory in alternative styles Soundness (all 7), Completeness (all 5), and TotalCorrectness (wpIsWeakest + wpLemma base cases) reworked with term-mode proofs, constructor-based structures, and direct field access. Plus mul4Inj and Assertion.impl_self in Exercises. Full project builds (853 jobs). --- CertIMP/Hoare/Completeness.lean | 36 +++++--------- CertIMP/Hoare/Exercises.lean | 8 +-- CertIMP/Hoare/Soundness.lean | 76 ++++++++++++----------------- CertIMP/Hoare/TotalCorrectness.lean | 31 +++++------- 4 files changed, 60 insertions(+), 91 deletions(-) diff --git a/CertIMP/Hoare/Completeness.lean b/CertIMP/Hoare/Completeness.lean index 503b837..e97c21c 100644 --- a/CertIMP/Hoare/Completeness.lean +++ b/CertIMP/Hoare/Completeness.lean @@ -15,37 +15,25 @@ def wlp (c : Com) (Q : Assertion) : Assertion := fun σ => ∀ σ', σ =[c]=> σ' → Q σ' lemma weakestPreSkip {w : Assertion} (h : isWeakestPre .CSkip Q w) : - w ->> Q := by - obtain ⟨parCorr, isWkst⟩ := h - intro σ h2 - exact parCorr σ σ .ESkip h2 + w ->> Q := + -- different: term-mode, via the structure's `isPartialCorrect` field + fun σ h2 => h.isPartialCorrect σ σ .ESkip h2 lemma weakestPreAsgn {w : Assertion} (h : isWeakestPre (.CAsgn x e) Q w) : - w ->> Q[e // x] := by - obtain ⟨parCorr, isWkst⟩ := h - intro σ h2 - exact parCorr σ (σ[x ↦ AExp.eval σ e]) (.EAsgn rfl rfl) h2 + w ->> Q[e // x] := + -- different: term-mode, via the structure's `isPartialCorrect` field + fun σ h2 => h.isPartialCorrect σ (σ[x ↦ AExp.eval σ e]) (.EAsgn rfl rfl) h2 -theorem wlpIsWp {c : Com} {Q : Assertion} : isWeakestPre c Q (wlp c Q) := by - apply isWeakestPre.mk - · intro σ σ' h1 h2 - simp only [wlp] at h2 - apply h2 - assumption - · intro P' h1 σ h2 - simp only [wlp] - intros - apply h1 - repeat assumption +theorem wlpIsWp {c : Com} {Q : Assertion} : isWeakestPre c Q (wlp c Q) := + -- different: build the structure directly with term-mode fields + ⟨fun _ σ' h1 h2 => h2 σ' h1, + fun {_} h1 σ h2 σ' h3 => h1 σ σ' h3 h2⟩ def Completeness : ⊨ ⦃ P ⦄ c ⦃ Q ⦄ → ⊢ ⦃ P ⦄ c ⦃ Q ⦄ := by + -- different: strengthen straight through `wlpIsWp.isWeakest` without unpacking intro h - have preWp : isWeakestPre c Q (wlp c Q) := wlpIsWp - obtain ⟨isPre, isWeakest⟩ := preWp - specialize isWeakest h - apply HPreStrengthen _ isWeakest - clear isWeakest isPre + apply HPreStrengthen _ (wlpIsWp.isWeakest h) cases c with | CSkip => apply @HPreStrengthen Q diff --git a/CertIMP/Hoare/Exercises.lean b/CertIMP/Hoare/Exercises.lean index c0f285e..5aad9ab 100644 --- a/CertIMP/Hoare/Exercises.lean +++ b/CertIMP/Hoare/Exercises.lean @@ -5,7 +5,8 @@ import Mathlib.Tactic.Linarith /- HELPERS -/ lemma mul4Inj {k n : ℕ} : ((4 * k) = (4 * n)) → k = n := by - aesop + -- different: arithmetic decision procedure instead of `aesop` + omega lemma consecutiveSquares {k n : ℕ} : (k * k ≤ n * n) → ((k+1) * (k+1) > n * n) → (k * k = n * n) := by @@ -38,8 +39,9 @@ def hoare_asgn_wrong : ∃ a, rfl · simp [State.init, Inhabited.default] -lemma Assertion.impl_self : P ->> P := by -verify_assertion +lemma Assertion.impl_self : P ->> P := + -- different: term-mode — implication reflexivity is just the identity + fun _ h => h def Hoare.HPreStrengthen : Proof P' c Q → (P ->> P') → Proof P c Q := by intro h1 h2 diff --git a/CertIMP/Hoare/Soundness.lean b/CertIMP/Hoare/Soundness.lean index 2085977..653ecc9 100644 --- a/CertIMP/Hoare/Soundness.lean +++ b/CertIMP/Hoare/Soundness.lean @@ -5,47 +5,37 @@ open BExp namespace Hoare -lemma hoare_skip : ⊨ ⦃ P ⦄ ⟨{ skip }⟩ ⦃ P ⦄ := by - intros σ σ' h p - cases h - assumption +lemma hoare_skip : ⊨ ⦃ P ⦄ ⟨{ skip }⟩ ⦃ P ⦄ := + -- different: term-mode, pattern-match the only constructor + fun _ _ h p => match h with | .ESkip => p lemma hoare_asgn : ⊨ ⦃ P[a // x] ⦄ ⟨{ ↑x = ↑a }⟩ ⦃ P ⦄ := by - intros σ σ' h p - cases h - case EAsgn n na σ'σ => - rw [σ'σ, na] - rw [Assertion.subst] at p - assumption + -- different: `subst` the result state, then rewrite via the value equation + intro σ σ' h p + cases h with + | EAsgn na σ'σ => + rw [Assertion.subst] at p + subst σ'σ + rwa [na] lemma hoare_seq (h₁ : ⊨ ⦃ P ⦄ c₁ ⦃ Q ⦄) (h₂ : ⊨ ⦃ Q ⦄ c₂ ⦃ R ⦄) : ⊨ ⦃ P ⦄ ⟨{ ↑c₁ ; ↑c₂}⟩ ⦃ R ⦄ := by - intros σ σ' h p - cases h - case ESeq σ'' σσ'' σ''σ' => - specialize h₁ σ σ'' σσ'' p - exact h₂ σ'' σ' σ''σ' h₁ + -- different: term-mode rebuild after destructuring the sequence + intro σ σ' h p + cases h with + | ESeq hc1 hc2 => exact h₂ _ _ hc2 (h₁ _ _ hc1 p) lemma hoare_if {b : BExp} (h₁ : ⊨ ⦃ P ∧ b ⦄ c₁ ⦃ Q ⦄) (h₂ : ⊨ ⦃ P ∧ ¬b ⦄ c₂ ⦃ Q ⦄) : ⊨ ⦃ P ⦄ ⟨{ if ↑b then ↑c₁ else ↑c₂ endif }⟩ ⦃ Q ⦄ := by - intros σ σ' h p - cases h - case EIfTrue bt c₁' => - specialize h₁ σ σ' c₁' - apply h₁ - unfold Assertion.and - exact And.intro p bt - case EIfFalse bf c₂' => - specialize h₂ σ σ' c₂' - apply h₂ - unfold Assertion.and - unfold Assertion.neg - simp only [Bool.not_eq_true] - exact And.intro p bf + -- different: term-mode, feed each branch's hypothesis the paired precondition + intro σ σ' h p + cases h with + | EIfTrue bt hc => exact h₁ σ σ' hc ⟨p, bt⟩ + | EIfFalse bf hc => exact h₂ σ σ' hc ⟨p, by simp [bf]⟩ lemma hoare_while {b : BExp} (h : ⊨ ⦃ P ∧ b ⦄ c ⦃ P ⦄) : @@ -60,7 +50,7 @@ lemma hoare_while {b : BExp} simp only [Bool.not_eq_true] rcases W with ⟨bb', _⟩ rw [bb'] - exact And.intro p bf + exact ⟨p, bf⟩ | @EWhileTrue σ'' c' σ''' b' σ'''' bt σ''σ''' σ'''σ'''' h' h'' => specialize h'' W apply h'' @@ -69,7 +59,7 @@ lemma hoare_while {b : BExp} rw [bb_cross, cc_cross] at h specialize h σ'' σ''' σ''σ''' unfold Assertion.and at h - exact h (And.intro p bt) + exact h ⟨p, bt⟩ | _ => aesop lemma hoare_consequence @@ -77,13 +67,9 @@ lemma hoare_consequence (hPost : Q' ->> Q) (hH : ⊨ ⦃ P' ⦄ c ⦃ Q' ⦄) : ⊨ ⦃ P ⦄ c ⦃ Q ⦄ := by - intros σ σ' h p - unfold Assertion.implies at hPre - unfold Assertion.implies at hPost - specialize hPre σ p - specialize hPost σ' - specialize hH σ σ' h hPre - exact hPost hH + -- different: term-mode composition of the three implications + intro σ σ' h p + exact hPost σ' (hH σ σ' h (hPre σ p)) def Soundness : ⊢ ⦃ P ⦄ c ⦃ Q ⦄ → ⊨ ⦃ P ⦄ c ⦃ Q ⦄ := by @@ -93,15 +79,13 @@ def Soundness : exact hoare_skip | HAsgn => exact hoare_asgn - | @HSeq P c₁ Q c₂ R _ _ ih₁ ih₂ => - apply hoare_seq - repeat assumption + | HSeq _ _ ih₁ ih₂ => + apply hoare_seq <;> assumption | HIf _ _ ih₁ ih₂ => - apply hoare_if ih₁ ih₂ + exact hoare_if ih₁ ih₂ | @HWhile P c b _ ih => - apply hoare_while ih - | HConsequence h₁ h₂ _ ih => - apply hoare_consequence - repeat assumption + exact hoare_while ih + | HConsequence _ _ _ ih => + apply hoare_consequence <;> assumption end Hoare diff --git a/CertIMP/Hoare/TotalCorrectness.lean b/CertIMP/Hoare/TotalCorrectness.lean index ab0fe6d..b949787 100644 --- a/CertIMP/Hoare/TotalCorrectness.lean +++ b/CertIMP/Hoare/TotalCorrectness.lean @@ -83,23 +83,22 @@ lemma wpLemma {pgm : Com} : exists σ'' | _ => contradiction | CSkip => + -- different: `constructor` + term-mode existential witnesses unfold wp - apply Iff.intro + constructor · intro h - exists σ - apply And.intro .ESkip h - · intro ⟨_, h1, _⟩ + exact ⟨σ, .ESkip, h⟩ + · rintro ⟨_, h1, h⟩ cases h1 - assumption + exact h | CAsgn x e => + -- different: `constructor` + term-mode existential witnesses unfold wp - apply Iff.intro + constructor · intro h unfold Assertion.subst at h - exists σ[x ↦ AExp.eval σ e] - apply And.intro _ h - apply EAsgn rfl rfl - · intro ⟨_, h, hq⟩ + exact ⟨σ[x ↦ AExp.eval σ e], EAsgn rfl rfl, h⟩ + · rintro ⟨_, h, hq⟩ cases h aesop | CSeq c₁ c₂ ih₁ ih₂ => @@ -145,13 +144,9 @@ lemma wpLemma {pgm : Com} : cases h₁ <;> aesop lemma wpIsWeakest {pgm : Com} : - isWeakestPre pgm Q (wp pgm Q) := by - apply isWeakestPre.mk - · intro σ - simp [wpLemma] - · intro P' h1 σ h2 - obtain ⟨σ', h3, h4⟩ := h1 σ h2 - rw [wpLemma] - exists σ' + isWeakestPre pgm Q (wp pgm Q) := + -- different: build the structure directly, threading `wpLemma` both ways + ⟨fun _ h => wpLemma.mp h, + fun {_} h1 σ h2 => wpLemma.mpr (h1 σ h2)⟩ end Total