delete deprecated EqnLemma and related defs/theorems

Author: alexkeizer

EffectSSA/ProofSketch/ProofSketch.lean

@@ -25,191 +25,6 @@ namespace EffectSSA.ProofSketch
 
 variable [SSA ι σ ν]
 
-/-!
-## Equation Lemma
--/
-section EqnLemma
-
-def Inst.EqnLemma (i : Inst ι) (x : VarId) (ρ : SEnv ι) : Prop :=
-  x ∈ i.results → (⟦i⟧ ρ).locals x = ρ.locals x
-
-@[grind] def InstSeq.EqnLemma (is : InstSeq ι) (x : VarId) (ρ : SEnv ι) : Prop :=
-  ∀ i ∈ is, Inst.EqnLemma i x ρ
-
-@[grind] def Pattern.EqnLemma (I : Pattern ι n) (x : VarId) (ρ : SEnv ι) : Prop :=
-  ∀ i ∈ I, InstSeq.EqnLemma i x ρ
-
--- TODO: HasEqn should probably be called WellBehaved or some such
-
-/--
-We say that an instruction `i` has a well-behaved equation lemma when:
-
-* validity of the equation lemma is stable under the execution of more instructions, and
-* executing `i` is guaranteed to yield an environment that satisfies its
-  own equation lemma
--/
-structure Inst.HasEqn (i : Inst ι) : Prop where
-  stable : ∀ x ρ, Inst.EqnLemma i x ρ → ∀ j : Inst ι, x ∉ j.results → Inst.EqnLemma i x (⟦j⟧ ρ)
-  idempotent : ∀ x ρ, Inst.EqnLemma i x (⟦i⟧ ρ)
-
-@[grind] def InstSeq.HasEqn (is : InstSeq ι) : Prop :=
-  ∀ i ∈ is, Inst.HasEqn i
-
-@[grind] def Pattern.HasEqn (I : Pattern ι n) : Prop :=
-  ∀ i ∈ I, InstSeq.HasEqn i
-
-section Lemmas
-variable {i : Inst ι} {is : InstSeq ι} {I : Pattern ι n}
-
-/-! vacuous -/
-
-@[grind =>] theorem Inst.eqnLemma_of_not_mem_results {ρ : SEnv ι} (hx : x ∉ i.results) :
-    EqnLemma i x ρ := by
-  grind [EqnLemma]
-
-@[grind =>] theorem InstSeq.eqnLemma_of_not_mem_results {ρ : SEnv ι} (hx : x ∉ is.results) :
-    EqnLemma is x ρ := by
-  intro i hi
-  grind
-
-@[grind =>] theorem Pattern.eqnLemma_of_not_mem_results {ρ : SEnv ι} (hx : x ∉ I.results) :
-    EqnLemma I x ρ := by
-  intro is his
-  grind
-
-/-! structural lemmas -/
-variable (I : Pattern ι n) (is : InstSeq ι)
-
-@[simp, grind .] theorem InstSeq.EqnLemma_nil {ρ : SEnv ι} :
-    InstSeq.EqnLemma ([] : InstSeq ι) x ρ := by
-  grind [InstSeq.EqnLemma]
-
-@[simp, grind =] theorem InstSeq.EqnLemma_cons {i : Inst ι} {is : InstSeq ι} {ρ : SEnv ι} :
-    InstSeq.EqnLemma (i ;> is) x ρ ↔ Inst.EqnLemma i x ρ ∧ InstSeq.EqnLemma is x ρ := by
-  grind [InstSeq.EqnLemma]
-
-variable {I} in
-@[grind .]
-theorem Pattern.eqnLemma_of_mem_results_get {k : Nat} {hk} {ρ : SEnv ι}
-    (hx : x ∈ I[k].results) (wf : I.NoShadowing):
-    Pattern.EqnLemma I x ρ ↔ InstSeq.EqnLemma I[k] x ρ := by
-  generalize hi : I[k] = is
-  constructor
-  · grind
-  · intro h js hj
-    by_cases is = js; grind
-    by_cases x ∈ is.results
-    · have : x ∉ js.results := by
-        have := results_disjoint_of_mem_of_noShadowing (by grind : is ∈ I) hj
-        grind
-      grind
-    · grind
-
-/-! stability -/
-
-attribute [grind =>] Inst.HasEqn.stable
-
-/--
-If `is.HasEqn`, then validity of the equation lemma is stable under the execution
-another instruction `j`.
--/
-@[grind =>]
-theorem InstSeq.eqnLemma_of_eqnLemma_inst {ρ : SEnv ι} (hEqn : HasEqn is) :
-    EqnLemma is x ρ → ∀ j : Inst ι, x ∉ j.results → EqnLemma is x (⟦j⟧ ρ) := by
-  grind
-
-/--
-If `I.HasEqn`, then validity of the equation lemma is stable under the execution
-another instruction `j`.
--/
-@[grind =>]
-theorem Pattern.eqnLemma_of_eqnLemma_inst {ρ : SEnv ι} (hEqn : HasEqn I) :
-    EqnLemma I x ρ → ∀ j : Inst ι, x ∉ j.results → EqnLemma I x (⟦j⟧ ρ) := by
-  grind
-
-/--
-If `I.HasEqn`, then validity of the equation lemma is stable under the execution
-another sequence of instructions `js`.
--/
-@[grind .]
-theorem Pattern.eqnLemma_of_eqnLemma_instSeq {ρ : SEnv ι} (hI : HasEqn I) :
-    EqnLemma I x ρ → ∀ js : InstSeq ι, x ∉ js.results → EqnLemma I x (⟦js⟧ ρ) := by
-  intro heqn js hjs
-  induction js generalizing ρ
-  · exact heqn
-  · grind
-
-/--
-If `i.HasEqn`, then validity of the equation lemma is stable under the execution
-another sequence of instructions `js`.
--/
-@[grind .]
-theorem Inst.eqnLemma_of_eqnLemma_instSeq {i : Inst ι} {ρ : SEnv ι} (hi : HasEqn i) :
-    EqnLemma i x ρ → ∀ js : InstSeq ι, x ∉ js.results → EqnLemma i x (⟦js⟧ ρ) := by
-  intro heqn js hjs
-  induction js generalizing ρ
-  · exact heqn
-  · grind
-
-/-! denote lemmas -/
-
-@[grind =] theorem Inst.locals_denote_of_eqnLemma {i : Inst ι} {ρ : SEnv ι}
-    (h : EqnLemma i x ρ) : (⟦i⟧ ρ).locals x = ρ.locals x := by
-  grind [EqnLemma]
-
-@[grind .] theorem InstSeq.locals_denote_of_eqnLemma {is : InstSeq ι} {ρ : SEnv ι}
-    (hEqn : HasEqn is)
-    (hwf : is.NoShadowing) (h : EqnLemma is x ρ) :
-    (⟦is⟧ ρ).locals x = ρ.locals x := by
-  induction is generalizing ρ
-  · rfl
-  · grind
-
-/-! idempotence -/
-
-attribute [grind .] Inst.HasEqn.idempotent
-
-/--
-If `is.HasEqn`, then evaluating `is` is guaranteed to yield an environment which
-satisfies its own equation lemma at any variable.
--/
-@[grind =>]
-theorem InstSeq.eqnLemma_denote_self {is : InstSeq ι} (hEqn : HasEqn is)
-    (hwf : is.NoShadowing) (ρ) :
-    EqnLemma is x (⟦is⟧ ρ) := by
-  induction is generalizing ρ
-  · simp
-  · simp; grind
-
-end Lemmas
-
-section EqnLemmaUpTo
-
-/--
-`I.usesAt v` is an alias of `I.collapse.usesAt v`.
-
-See `InstSeq.usesAt` for details.
--/
-abbrev Pattern.usesAt (v : VarId) (I : Pattern ι n) := I.collapse.usesAt v
-
-/--
-`I.getDef? v` is an alias of `I.collapse.getDef? v`.
-
-See `InstSeq.getDef?` for details.
--/
-abbrev Pattern.getDef? (v : VarId) (I : Pattern ι n) :=
-  I.collapse.getDef? v
-
-/--
-`I.EqnLemmaUpTo h ρ` holds when `ρ` satisfies the equation lemma for all
-(transitive) dependencies of the `h`-th pattern of `I`.
--/
-def Pattern.EqnLemmaUpTo (I : Pattern ι n) (h : Hole n) (ρ : SEnv ι) : Prop :=
-  ∀ x ∈ I[h].args,
-    ∀ y, y = x ∨ y ∈ (I.usesAt x) → Pattern.EqnLemma I y ρ
-
-end EqnLemmaUpTo
-end EqnLemma
 
 /-!
 ## Denotational Refinement & Equivalence
@@ -256,47 +71,6 @@ def Pattern.CtxRefine (I J : Pattern ι n) : Prop :=
     CI.WellFormed ∅ → CJ.WellFormed ∅ →
       ⟦CI⟧ {} ⊒ ⟦CJ⟧ {}
 
-/-!
-## Residual
--/
-section Residual
-
-/--
-We say that `Γ` is a residual of context `C` under pattern `I` when
-
-TODO: dedup with Invariant
--/
-@[grind, grind cases]
-private structure Residual (Γ : VarSet) (C : MultiContext ι n) (P : Pattern ι n) : Prop where
-  /-- `H` is the list of previously seen holes -/
-  residual : ∃ H : List (Hole n), C.CompleteMod H ∧ ∀ h ∈ H, P[h].results ⊆ Γ
-  /-- `C.plug I` is well-formed with free variables `Γ`. -/
-  wf : (C.plug P).WellFormed Γ
-
-namespace Residual
-variable {Γ : VarSet} {C : MultiContext ι n} {P : Pattern ι n} {i : Inst ι} {h : Hole n}
-
-/-! invariants -/
-
-private theorem initial (wf : (C.plug P).WellFormed ∅) (hC : C.Complete) : Residual ∅ C P := by
-  grind [Pattern.mem_iff_getElem_hole, MultiContext.CompleteMod]
-
-@[grind →] private theorem of_cons_inst :
-    Residual Γ (.inl i :: C) P → Residual (i.resultsSet ∪ Γ) C P := by
-  rintro ⟨wf, residual⟩;
-  constructor
-  · simp_all; grind
-  · simp_all
-
-@[grind →] private theorem of_cons_hole  :
-    Residual Γ (.inr h :: C) P → Residual (P[h].results ∪ Γ) C P := by
-  rintro ⟨wf, residual⟩; constructor
-  · simp_all; grind
-  · simp_all
-
-end Residual
-end Residual
-
 /-!
 ## Main Result for straight-line programs
 -/