From c32dc4a84530aac4d2341c3912f5fab714ef9657 Mon Sep 17 00:00:00 2001 From: "E. Prebet" Date: Mon, 15 Jun 2026 18:08:17 +0200 Subject: [PATCH 1/3] One-pass for Term --- DLean/USubst/Semantics.lean | 165 ++++++++++++++++++------------------ DLean/USubst/Subst.lean | 36 ++++---- 2 files changed, 101 insertions(+), 100 deletions(-) diff --git a/DLean/USubst/Semantics.lean b/DLean/USubst/Semantics.lean index 2e42938..ae4bff5 100644 --- a/DLean/USubst/Semantics.lean +++ b/DLean/USubst/Semantics.lean @@ -333,11 +333,12 @@ theorem subst_adjoint_of_term_vector_to_subst theorem Subst.apply_subst_term_vector_to_term (σ : Subst) + (U : FCSet Assignable) {n : ℕ} (args a : TermVector n) (x : Fin n) - : TermVector.applySubst σ args = some a - → Term.applySubst σ args.toVector[x] = some a.toVector[x] := by + : TermVector.applySubst σ U args = some a + → Term.applySubst σ U args.toVector[x] = some a.toVector[x] := by intro h cases args with | nil => grind @@ -395,9 +396,9 @@ theorem toSubst.freeVars_inc {n : ℕ} (args : TermVector n) (S : Option (Finset mutual -theorem TermVector.freeVars_applySubst_subset {n : ℕ} (σ : Subst) (ts as : TermVector n) - : TermVector.applySubst σ ts = some as - → ↑as.freeVars ⊆ ↑ts.freeVars ∪ (σ.freeVars (some ts.signature)).toSet := by +theorem TermVector.freeVars_applySubst_subset {n : ℕ} (σ : Subst) (U : FCSet Assignable) (ts as : TermVector n) + : TermVector.applySubst σ U ts = some as + → ↑as.freeVars ⊆ ↑ts.freeVars ∪ (σ.freeVars (some ts.signature) \ U).toSet := by intro h₁ match n with | 0 => @@ -418,17 +419,17 @@ theorem TermVector.freeVars_applySubst_subset {n : ℕ} (σ : Subst) (ts as : Te clear h₁ simp only [TermVector.freeVars_cons, Finset.coe_union, TermVector.signature_cons] have := @σ.freeVars_symbol_union t.signature ts'.signature - have := Term.freeVars_applySubst_subset σ t a heqa - have := TermVector.freeVars_applySubst_subset σ ts' as' heqas' - grind only [= Set.mem_union, = Set.subset_def] + have := Term.freeVars_applySubst_subset σ U t a heqa + have := TermVector.freeVars_applySubst_subset σ U ts' as' heqas' + grind only [= Set.subset_def, FCSet.to_set_diff, = Set.mem_union, = Set.mem_diff] termination_by (σ.size, sizeOf ts) decreasing_by all_goals simp_wf all_goals grind only [= Prod.lex_def] -theorem Term.freeVars_applySubst_subset (σ : Subst) (t a : Term) - : Term.applySubst σ t = some a - → ↑a.freeVars ⊆ ↑t.freeVars ∪ (σ.freeVars (some t.signature)).toSet := by +theorem Term.freeVars_applySubst_subset (σ : Subst) (U : FCSet Assignable) (t a : Term) + : Term.applySubst σ U t = some a + → ↑a.freeVars ⊆ ↑t.freeVars ∪ (σ.freeVars (some t.signature) \ U).toSet := by intro h₁ match t with | .var v => simp_all[Term.applySubst] @@ -437,7 +438,7 @@ theorem Term.freeVars_applySubst_subset (σ : Subst) (t a : Term) split at h₁ . contradiction next a' heq => - have := Term.freeVars_applySubst_subset σ t a' heq + have := Term.freeVars_applySubst_subset σ U t a' heq simp_all rw[← h₁] simp only[Term.freeVars, Term.signature] @@ -452,21 +453,19 @@ theorem Term.freeVars_applySubst_subset (σ : Subst) (t a : Term) . contradiction next b heqb _ _ c heqc => simp_all only [Term.signature] - have := Term.freeVars_applySubst_subset σ t₁ b heqb - have := Term.freeVars_applySubst_subset σ t₂ c heqc + have := Term.freeVars_applySubst_subset σ U t₁ b heqb + have := Term.freeVars_applySubst_subset σ U t₂ c heqc simp[Term.freeVars] all_goals simp at h₁ rw[← h₁] simp[Term.freeVars] have := @Subst.freeVars_symbol_union σ t₁.signature t₂.signature - grind only [= Set.mem_union, = Set.subset_def] + grind only [= Set.subset_def, FCSet.to_set_diff, = Set.mem_union, = Set.mem_diff] | .applyFn f args => match f with | .num n => - simp[Term.applySubst, Option.bind] at h₁ - split at h₁ - . contradiction + simp[Term.applySubst] at h₁ simp_all | .sym s => simp_all only [Term.freeVars, Term.signature] @@ -477,62 +476,66 @@ theorem Term.freeVars_applySubst_subset (σ : Subst) (t a : Term) split at h₁ . simp at h₁ - have := TermVector.freeVars_applySubst_subset σ args a' (by assumption) - have := Term.freeVars_applySubst_subset a'.toSubst (σ.get (Symbol.Function s)) a h₁ - have := @toSubst.freeVars_inc _ a' (some (Term.signature (σ.get (Symbol.Function s)))) - have := @Subst.freeVars_symbol_union σ (Function.signature (Fn.sym s)) args.signature - have := @Subst.free_vars_subset_fun σ s - grind only [= Set.mem_union, = Set.subset_def, FCSet.to_set_eq] + split at h₁ + . contradiction + next _ heq => + simp at h₁ heq + have := TermVector.freeVars_applySubst_subset σ U args a' (by assumption) + have := Term.freeVars_applySubst_subset a'.toSubst ∅ (σ.get (Symbol.Function s)) a h₁ + have := @toSubst.freeVars_inc _ a' (some (Term.signature (σ.get (Symbol.Function s)))) + have := @Subst.freeVars_symbol_union σ (Function.signature (Fn.sym s)) args.signature + have := @Subst.free_vars_subset_fun σ s + simp_all only [←Set.disjoint_iff_inter_eq_empty] + grind only [= Set.disjoint_left, = Set.subset_def, FCSet.to_set_diff, + = Set.mem_union, = Set.mem_diff] . simp at h₁ rw[← h₁] simp[Term.freeVars] - have := TermVector.freeVars_applySubst_subset σ args a' (by assumption) + have := TermVector.freeVars_applySubst_subset σ U args a' (by assumption) have := @Subst.freeVars_symbol_union σ - grind only [= Set.mem_union, = Set.subset_def] + grind only [= Set.subset_def, FCSet.to_set_diff, = Set.mem_union, = Set.mem_diff] | .differential t => simp[Term.applySubst, Option.bind] at h₁ split at h₁ . contradiction simp at h₁ - split at h₁ - . contradiction - next _ _ hg _ _ a' heq => - simp at h₁ hg + next a' heq => rw[←h₁] clear h₁ - have := Term.freeVars_applySubst_subset σ _ _ heq - simp only [Term.freeVars, Finset.coe_union, Finset.coe_map, Term.signature] - grind only [= Set.mem_image, = Set.mem_empty_iff_false, = Set.mem_union, = Set.subset_def] + have := Term.freeVars_applySubst_subset σ .univ _ _ heq + simp only [Term.freeVars, Finset.coe_union, Finset.coe_map, Term.signature, FCSet.to_set_diff, FCSet.to_set_univ, Set.diff_univ, Set.union_empty] at * + grind only [= Set.mem_diff, = Set.mem_image, = Set.mem_union, = Set.subset_def] termination_by (σ.size, sizeOf t) decreasing_by all_goals simp_wf all_goals (try grind only [= Prod.lex_def]) -next hin => +next hin _ _ _ _ _ => rw[TermVector.toSubst_size] apply Subst.symbol_size at hin grind only [= Prod.lex_def] end theorem Term.freeVars_applySubst_admissible_univ_subset (σ : Subst) (t a : Term) - : Term.applySubst σ t = some a - → σ.admissible FCSet.univ t.signature + : Term.applySubst σ FCSet.univ t = some a → (a.freeVars : Set Assignable ) ⊆ (t.freeVars : Set Assignable) := by intros h _ - have := Term.freeVars_applySubst_subset σ t a h - simp_all only [FCSet.to_set_eq, FCSet.to_set_inter, FCSet.to_set_univ, Set.inter_univ, - FCSet.to_set_empty, Set.union_empty, Finset.coe_subset] - + have := Term.freeVars_applySubst_subset σ FCSet.univ t a h + simp only [FCSet.to_set_diff, FCSet.to_set_univ, Set.diff_univ, Set.union_empty, + SetLike.coe_subset_coe, Finset.le_eq_subset] at this + apply this theorem Subst.preserve_semantics.term (σ : Subst) + (U : FCSet Assignable) (i : Interpretation) - (v : State) + (v w : State) + (hvw : v.isEqExcept w U) (t t' : Term) - (hs : t' = Term.applySubst σ t) - : Term.denote i v t' = Term.denote (Subst.adjoint σ i v) v t := by + (hs : t' = Term.applySubst σ U t) + : Term.denote i v t' = Term.denote (Subst.adjoint σ i w) v t := by match t with | .var x => simp_all[Term.applySubst, Term.denote] | .neg t => @@ -541,7 +544,7 @@ theorem Subst.preserve_semantics.term . contradiction . next a heq => - have := Subst.preserve_semantics.term σ i v t a (by simp[heq]) + have := Subst.preserve_semantics.term σ U i v w hvw t a (by simp[heq]) simp_all[Term.denote] | .plus t₁ t₂ | .times t₁ t₂ => @@ -554,15 +557,13 @@ theorem Subst.preserve_semantics.term . contradiction . next a ha _ _ b hb => - have := Subst.preserve_semantics.term σ i v t₁ a (by simp[ha]) - have := Subst.preserve_semantics.term σ i v t₂ b (by simp[hb]) + have := Subst.preserve_semantics.term σ U i v w hvw t₁ a (by simp[ha]) + have := Subst.preserve_semantics.term σ U i v w hvw t₂ b (by simp[hb]) simp_all[Term.denote] | .applyFn f args => match hf : f with | .num n => - simp[Term.applySubst, Option.bind] at hs - split at hs - . contradiction + simp[Term.applySubst] at hs simp_all[Term.denote] | .sym s => simp[Term.applySubst, Option.bind] at hs @@ -570,41 +571,48 @@ theorem Subst.preserve_semantics.term . contradiction . - simp_all + simp at hs -- we do apply the subst split at hs next _ b _ _ => - + split at hs + . contradiction + simp_all simp[Term.denote] -- remove adjoint by Subst.preserve_semantics.termVector have : (fun (x : Fin s.arity) => - Term.denote (σ.adjoint i v) v args.toVector[↑(x : Nat)]) + Term.denote (σ.adjoint i w) v args.toVector[↑(x : Nat)]) = (fun (x : Fin s.arity) => Term.denote i v b.toVector[↑x]) := by funext x apply Eq.symm - apply Subst.preserve_semantics.term + apply Subst.preserve_semantics.term _ _ _ _ _ hvw apply Eq.symm apply Subst.apply_subst_term_vector_to_term assumption rw[this] - apply Subst.preserve_semantics.term b.toSubst at hs - rw[hs] - rw[subst_adjoint_of_term_vector_to_subst] - simp only [adjoint] - + apply Subst.preserve_semantics.term b.toSubst _ _ v v at hs + . + rw[hs] + rw[subst_adjoint_of_term_vector_to_subst] + simp only [adjoint] + apply Term.coincidence + simp_all[State.isEqExcept, ←Set.disjoint_iff_inter_eq_empty] + grind only [= Set.disjoint_left, Set.EqOn, = Set.mem_compl_iff] + . + simp_all only [State.isEqExcept, FCSet.to_set_empty, Set.compl_empty, Set.eqOn_univ] next a _ _ => -- we don't apply subst simp_all -- remove adjoint by Subst.preserve_semantics.termVector have : (fun (x : Fin s.arity) => - Term.denote (σ.adjoint i v) v args.toVector[↑(x : ℕ)]) + Term.denote (σ.adjoint i w) v args.toVector[↑(x : ℕ)]) = (fun (x : Fin s.arity) => Term.denote i v a.toVector[↑x]) := by funext x apply Eq.symm - apply Subst.preserve_semantics.term + apply Subst.preserve_semantics.term _ _ _ _ _ hvw apply Eq.symm apply Subst.apply_subst_term_vector_to_term assumption @@ -612,18 +620,15 @@ theorem Subst.preserve_semantics.term simp[Term.denote] rw[this] - -- remove remaining adjoint because `σ.adjoint i v f = i f` if `f ∉ σ` - have := @Subst.adjoint_noeffect_nomem_fun i v s σ (by assumption) + -- remove remaining adjoint because `σ.adjoint i w f = i f` if `f ∉ σ` + have := @Subst.adjoint_noeffect_nomem_fun i w s σ (by assumption) rw[this] simp | .differential t => simp[Term.applySubst, Option.bind] at hs split at hs . contradiction - simp at hs - split at hs - . contradiction - next _ _ hg _ _ a heq => + next a heq => simp at hs cases hs simp[Term.denote] @@ -652,7 +657,7 @@ theorem Subst.preserve_semantics.term -- and hence substitution can *only reduce* free variables, e.g. {f(⋅) → 2} have : a.freeVars ⊆ t.freeVars := by have ih := Term.freeVars_applySubst_admissible_univ_subset - (σ := σ) t a heq (by simp_all[Subst.admissible]) + (σ := σ) t a heq intro x hx have := ih hx grind @@ -669,14 +674,10 @@ theorem Subst.preserve_semantics.term funext x congr funext y - have := by - apply @Subst.admissible_adjoint.term v (v.update x y) (v.update x y) σ i t FCSet.univ - . simp_all[Subst.admissible, Option.guard_eq_some'] - . simp_all[State.isEqOn] - rw[this] + apply Subst.preserve_semantics.term _ FCSet.univ + . simp only [FCSet.to_set_univ, State.eq_except_univ] + . simp_all only - apply Subst.preserve_semantics.term σ i (v.update x y) - grind termination_by (σ.size, sizeOf t) decreasing_by @@ -703,12 +704,12 @@ lemma ode_mapM_assignables_eq {σ : Subst} {system : OdeSystem} {ssystem : OdeSystem} - (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ x.term)) + (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ ∅ x.term)) = some ssystem) : OdeSystem.assignables ssystem = OdeSystem.assignables system := by unfold OdeSystem.assignables at *; induction system generalizing ssystem <;> simp_all +decide [ List.mapM_cons ]; - cases h' : Term.applySubst σ ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; + cases h' : Term.applySubst σ ∅ ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; aesop lemma ode_evolution_formula_applySubst @@ -716,7 +717,7 @@ lemma ode_evolution_formula_applySubst {system ssystem : OdeSystem} {Ψ Ψ' : Formula} : Formula.applySubst σ Ψ = some Ψ' - → system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ x.term)) = some ssystem + → system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ ∅ x.term)) = some ssystem → Formula.applySubst σ (odeEvolutionFormula system Ψ) = some (odeEvolutionFormula ssystem Ψ') := by @@ -724,7 +725,7 @@ lemma ode_evolution_formula_applySubst induction system generalizing ssystem Ψ Ψ' with | nil => simp_all[odeEvolutionFormula] | cons head tail ih => - cases _ : Term.applySubst σ head.term + cases _ : Term.applySubst σ ∅ head.term . simp_all . simp_all[Option.bind_eq_some_iff] @@ -782,8 +783,8 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all[Formula.denote] - have := Subst.preserve_semantics.term σ i v t₁ - have := Subst.preserve_semantics.term σ i v t₂ + have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t₁ + have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t₂ grind | .not Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] @@ -943,7 +944,7 @@ theorem Subst.preserve_semantics.formula = (fun (x : Fin p.arity) => Term.denote i v args'.toVector[↑x]) := by funext x apply Eq.symm - apply Subst.preserve_semantics.term + apply Subst.preserve_semantics.term _ ∅ _ _ _ (Set.eqOn_refl _ _) apply Eq.symm apply Subst.apply_subst_term_vector_to_term assumption @@ -990,7 +991,7 @@ theorem Subst.preserve_semantics.program . contradiction rename Term => t' simp_all[Program.denote] - have := Subst.preserve_semantics.term σ i v t t' + have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t t' grind | .random x => simp[Program.applySubst] at hs diff --git a/DLean/USubst/Subst.lean b/DLean/USubst/Subst.lean index 67fe6fe..e1a0815 100644 --- a/DLean/USubst/Subst.lean +++ b/DLean/USubst/Subst.lean @@ -212,33 +212,33 @@ termination_by mutual -def TermVector.applySubst {n : ℕ} (σ : Subst) (ts : TermVector n) : Option (TermVector n) := +def TermVector.applySubst {n : ℕ} (σ : Subst) (U : FCSet Assignable) (ts : TermVector n) : Option (TermVector n) := match ts with | .nil => pure .nil | .cons t ts => do - return .cons (← Term.applySubst σ t) (← TermVector.applySubst σ ts) + return .cons (← Term.applySubst σ U t) (← TermVector.applySubst σ U ts) termination_by (σ.size, sizeOf ts) decreasing_by all_goals simp_wf all_goals grind only [= Prod.lex_def] -def Term.applySubst (σ : Subst) (t : Term) : Option Term := +def Term.applySubst (σ : Subst) (U : FCSet Assignable) (t : Term) : Option Term := match t with | .var x => return .var x - | .neg t' => do return .neg (← Term.applySubst σ t') - | .plus t₁ t₂ => do return .plus (← Term.applySubst σ t₁) (← Term.applySubst σ t₂) - | .times t₁ t₂ => do return .times (← Term.applySubst σ t₁) (← Term.applySubst σ t₂) + | .neg t' => do return .neg (← Term.applySubst σ U t') + | .plus t₁ t₂ => do return .plus (← Term.applySubst σ U t₁) (← Term.applySubst σ U t₂) + | .times t₁ t₂ => do return .times (← Term.applySubst σ U t₁) (← Term.applySubst σ U t₂) | .differential t => do - guard <| σ.admissible .univ t.signature - return .differential (← Term.applySubst σ t) - | .applyFn (.num n) args => do - let sargs ← TermVector.applySubst σ args - return .applyFn (.num n) sargs + return .differential (← Term.applySubst σ .univ t) + | .applyFn (.num _) _ => do + -- let sargs ← TermVector.applySubst σ U args + return t | .applyFn (.sym f) args => do - let sargs ← TermVector.applySubst σ args + let sargs ← TermVector.applySubst σ U args if (.Function f) ∈ σ then - Term.applySubst (sargs.toSubst) (Subst.get σ f) + guard <| .Finite (Subst.get σ f).freeVars ∩ U = ∅ + Term.applySubst (sargs.toSubst) ∅ (Subst.get σ f) else return .applyFn (.sym f) sargs @@ -258,8 +258,8 @@ mutual def Formula.applySubst (σ : Subst) (Φ : Formula) : Option Formula := match Φ with | .True | .False => Φ - | .eq t₁ t₂ => do return .eq (← t₁.applySubst σ) (← t₂.applySubst σ) - | .gte t₁ t₂ => do return .gte (← t₁.applySubst σ) (← t₂.applySubst σ) + | .eq t₁ t₂ => do return .eq (← t₁.applySubst σ ∅) (← t₂.applySubst σ ∅) + | .gte t₁ t₂ => do return .gte (← t₁.applySubst σ ∅) (← t₂.applySubst σ ∅) | .not Φ' => do return .not (← Φ'.applySubst σ) | .and Φ₁ Φ₂ => do return .and (← Φ₁.applySubst σ) (← Φ₂.applySubst σ) | .forall x Φ => do @@ -281,7 +281,7 @@ def Formula.applySubst (σ : Subst) (Φ : Formula) : Option Formula := match Φ | .ref α β => do return .ref (← α.applySubst σ) (← β.applySubst σ) | .applyPred p args => do - let sargs ← TermVector.applySubst σ args + let sargs ← TermVector.applySubst σ ∅ args if (.Predicate p) ∈ σ then Formula.applySubst (sargs.toSubst) (Subst.get σ p) else @@ -295,7 +295,7 @@ next hin => grind only [= Prod.lex_def] def Program.applySubst (σ : Subst) (α : Program) : Option Program := match α with - | .assign x t => return .assign x (← t.applySubst σ) + | .assign x t => return .assign x (← t.applySubst σ ∅) | .random x => return .random x | .test Φ => return .test (← Φ.applySubst σ) | .ode system Ψ => do @@ -307,7 +307,7 @@ def Program.applySubst (σ : Subst) (α : Program) : Option Program := match α guard <| σ.admissible (.Finite (vars ∪ vars')) Ψ.signature guard <| terms.all (σ.admissible (.Finite (vars ∪ vars')) ∘ Term.signature) - let ssystem ← system.mapM (fun {var, term} => do return ODE.mk var (← Term.applySubst σ term)) + let ssystem ← system.mapM (fun {var, term} => do return ODE.mk var (← Term.applySubst σ ∅ term)) return .ode ssystem σΨ | .choice α β => return .choice (← α.applySubst σ) (← β.applySubst σ) | .seq α β => do From 08e11f0621e71aa9ffb5fbab5ef631ce582215c0 Mon Sep 17 00:00:00 2001 From: "E. Prebet" Date: Tue, 16 Jun 2026 15:56:04 +0200 Subject: [PATCH 2/3] One-pass without bound calc --- DLean/USubst/Semantics.lean | 465 +++++++++++++++++------------------- DLean/USubst/Subst.lean | 223 ++++++++++++++--- 2 files changed, 402 insertions(+), 286 deletions(-) diff --git a/DLean/USubst/Semantics.lean b/DLean/USubst/Semantics.lean index ae4bff5..857bdd2 100644 --- a/DLean/USubst/Semantics.lean +++ b/DLean/USubst/Semantics.lean @@ -702,30 +702,32 @@ decreasing_by lemma ode_mapM_assignables_eq {σ : Subst} + {U : FCSet Assignable} {system : OdeSystem} {ssystem : OdeSystem} - (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ ∅ x.term)) + (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some ssystem) : OdeSystem.assignables ssystem = OdeSystem.assignables system := by unfold OdeSystem.assignables at *; induction system generalizing ssystem <;> simp_all +decide [ List.mapM_cons ]; - cases h' : Term.applySubst σ ∅ ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; + cases h' : Term.applySubst σ U ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; aesop lemma ode_evolution_formula_applySubst {σ : Subst} + {U : FCSet Assignable} {system ssystem : OdeSystem} {Ψ Ψ' : Formula} - : Formula.applySubst σ Ψ = some Ψ' - → system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ ∅ x.term)) = some ssystem - → Formula.applySubst σ (odeEvolutionFormula system Ψ) + : Formula.applySubst σ U Ψ = some Ψ' + → system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some ssystem + → Formula.applySubst σ U (odeEvolutionFormula system Ψ) = some (odeEvolutionFormula ssystem Ψ') := by intros h₁ h₂ induction system generalizing ssystem Ψ Ψ' with | nil => simp_all[odeEvolutionFormula] | cons head tail ih => - cases _ : Term.applySubst σ ∅ head.term + cases _ : Term.applySubst σ U head.term . simp_all . simp_all[Option.bind_eq_some_iff] @@ -758,6 +760,77 @@ lemma ode_evolution_formula_admissible unfold Subst.admissible; aesop; exact h_foldr system hterms +lemma Program.boundVars_applySubst_subset + (σ : Subst) + (U : FCSet Assignable) + (α α' : Program) : + Program.applySubst σ U α = α' → α'.boundVars ⊆ α.boundVars := by + intro h + match α with + | .const a => + simp[Program.boundVars] + | .test _ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp at h + rw[←h] + simp[Program.boundVars] + | .assign _ _ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp at h + rw[←h] + simp[Program.boundVars] + | .random _ => + simp[Program.applySubst] at h + rw[←h] + | .choice β γ + | .seq β γ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp only at h + split at h + . contradiction + simp at h + next β' hβ _ _ γ' hγ => + apply Program.boundVars_applySubst_subset at hγ + apply Program.boundVars_applySubst_subset at hβ + grind only [= Set.subset_def, boundVars, = Set.mem_union] + | .loop β => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp only at h + split at h + . contradiction + simp at h + next β' hβ => + apply Program.boundVars_applySubst_subset at hβ + grind only [boundVars] + | .ode sys _ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp only at h + split at h + . contradiction + simp at h + next sys' hsys => + have hassign : OdeSystem.assignables sys' = OdeSystem.assignables sys := + ode_mapM_assignables_eq (show _ = some sys' from ‹_›) + grind only [boundVars, = Set.subset_def] + +lemma Program.boundVars'_applySubst_subset + (σ : Subst) + (U : FCSet Assignable) + (α α' : Program) : + Program.applySubst σ U α = α' → α'.boundVars'.toSet ⊆ α.boundVars'.toSet := by + rw[←Program.bound_vars_decidable α, ←Program.bound_vars_decidable α'] + apply Program.boundVars_applySubst_subset + set_option maxHeartbeats 0 in /- Good things take time (dunno if that is one of them) --/ @@ -765,11 +838,13 @@ mutual theorem Subst.preserve_semantics.formula (σ : Subst) + (U : FCSet Assignable) (i : Interpretation) - (v : State) + (v w : State) + (hvw : v.isEqExcept w U) (Φ Φ' : Formula) - (hs : Φ' = Formula.applySubst σ Φ) - : v ∈ Formula.denote i Φ' ↔ v ∈ Formula.denote (Subst.adjoint σ i v) Φ := by + (hs : Φ' = Formula.applySubst σ U Φ) + : v ∈ Formula.denote i Φ' ↔ v ∈ Formula.denote (Subst.adjoint σ i w) Φ := by match Φ with | .True | .False => @@ -783,8 +858,8 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all[Formula.denote] - have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t₁ - have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t₂ + have := Subst.preserve_semantics.term σ U i v w hvw t₁ + have := Subst.preserve_semantics.term σ U i v w hvw t₂ grind | .not Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] @@ -792,7 +867,7 @@ theorem Subst.preserve_semantics.formula . contradiction simp_all rename Formula => Φ' - have := Subst.preserve_semantics.formula σ i v Φ Φ' + have := Subst.preserve_semantics.formula σ U i v w hvw Φ Φ' simp_all[Formula.denote] | .and Φ₁ Φ₂ => simp_all[Formula.denote, Formula.applySubst, Option.bind] @@ -803,69 +878,46 @@ theorem Subst.preserve_semantics.formula . contradiction simp_all next Φ₁' _ _ _ Φ₂' _ => - have := Subst.preserve_semantics.formula σ i v Φ₁ Φ₁' - have := Subst.preserve_semantics.formula σ i v Φ₂ Φ₂' + have := Subst.preserve_semantics.formula σ U i v w hvw Φ₁ Φ₁' + have := Subst.preserve_semantics.formula σ U i v w hvw Φ₂ Φ₂' simp_all[Formula.denote] | .forall x Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] split at hs . contradiction simp_all - split at hs - . contradiction rename Formula => Φ' simp_all[Formula.denote] apply Iff.intro . intros h r - have := (Subst.preserve_semantics.formula σ i (v.update x r) Φ Φ' (by grind)).mp (h r) - have := Subst.admissible_adjoint.formula (U := {.var x}) (Φ := Φ) (i := i) (σ := σ) - (v := v) (w := v.update x r) - (by simp_all[Subst.admissible]) - (by simp_all[State.isEqOn, Set.EqOn]) - rw[this] - grind + have hvw' : (v.update x r).isEqExcept w ({.var x} ∪ U).toSet := by grind[Set.EqOn, State.isEqExcept] + apply (Subst.preserve_semantics.formula σ ({.var x} ∪ U) i (v.update x r) w hvw' Φ Φ' (by grind)).mp (h r) + . intros h r - have := Subst.admissible_adjoint.formula (U := {.var x}) (Φ := Φ) (i := i) (σ := σ) - (v := v) (w := v.update x r) - (by simp_all[Subst.admissible]) - (by simp_all[State.isEqOn, Set.EqOn]) - rw[this] at h - have := (Subst.preserve_semantics.formula σ i (v.update x r) Φ Φ' (by grind)).mpr (h r) - grind + have hvw' : (v.update x r).isEqExcept w ({.var x} ∪ U).toSet := by grind[Set.EqOn, State.isEqExcept] + apply (Subst.preserve_semantics.formula σ ({.var x} ∪ U) i (v.update x r) w hvw' Φ Φ' (by grind)).mpr (h r) | .exists x Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] split at hs . contradiction simp_all - split at hs - . contradiction rename Formula => Φ' simp_all[Formula.denote] apply Iff.intro . - intros h - obtain ⟨r, hr⟩ := h + intro ⟨r, hr⟩ apply Exists.intro r - have := Subst.preserve_semantics.formula σ i (v.update x r) Φ Φ' (by grind) - have := Subst.admissible_adjoint.formula (U := {.var x}) (Φ := Φ) (i := i) (σ := σ) - (v := v) (w := v.update x r) - (by simp_all[Subst.admissible]) - (by simp_all[State.isEqOn, Set.EqOn]) - grind + have hvw' : (v.update x r).isEqExcept w ({.var x} ∪ U).toSet := by grind[Set.EqOn, State.isEqExcept] + apply (Subst.preserve_semantics.formula σ ({.var x} ∪ U) i (v.update x r) w hvw' Φ Φ' (by grind)).mp hr . - intros h - obtain ⟨r, hr⟩ := h + intro ⟨r, hr⟩ apply Exists.intro r - have := Subst.preserve_semantics.formula σ i (v.update x r) Φ Φ' (by grind) - have := Subst.admissible_adjoint.formula (U := {.var x}) (Φ := Φ) (i := i) (σ := σ) - (v := v) (w := v.update x r) - (by simp_all[Subst.admissible]) - (by simp_all[State.isEqOn, Set.EqOn]) - grind + have hvw' : (v.update x r).isEqExcept w ({.var x} ∪ U).toSet := by grind[Set.EqOn, State.isEqExcept] + apply (Subst.preserve_semantics.formula σ ({.var x} ∪ U) i (v.update x r) w hvw' Φ Φ' (by grind)).mpr hr | .box α Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] split at hs @@ -874,24 +926,22 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all - split at hs - . contradiction rename Program => α' rename Formula => Φ' simp_all[Formula.denote] + set V := α'.boundVars' ∪ U apply Iff.intro all_goals - -- guard <| σ.admissible σα.boundVars' Φ.signature - intros h₁ w h₂ - have := Program.bound_effect h₂ - have := Subst.preserve_semantics.program σ i v w α α' - have := Subst.admissible_adjoint.formula (U := α'.boundVars') - (Φ := Φ) (i := i) - (σ := σ) (v := v) (w := w) - (by simp_all[Subst.admissible]) - (by grind[Program.bound_effect']) - have := Subst.preserve_semantics.formula σ i w Φ Φ' - grind + intros h₁ w' h₂ + have := Subst.preserve_semantics.program σ U i v w w' hvw α α' + simp_all only [iff_true, forall_const] + have := Program.bound_effect this + rw[Program.bound_vars_decidable α'] at this + have hww' : w'.isEqExcept w V.toSet := by + grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + = Set.mem_union] + have := Subst.preserve_semantics.formula σ V i w' w hww' Φ Φ' + grind only | .diamond α Φ => simp_all[Formula.denote, Formula.applySubst, Option.bind] split at hs @@ -900,24 +950,23 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all - split at hs - . contradiction rename Program => α' rename Formula => Φ' simp_all[Formula.denote] + set V := α'.boundVars' ∪ U apply Iff.intro all_goals - intros h - obtain ⟨w, hw⟩ := h - apply Exists.intro w - have := Subst.preserve_semantics.program σ i v w α α' - have := Subst.admissible_adjoint.formula (U := α'.boundVars') - (Φ := Φ) (i := i) - (σ := σ) (v := v) (w := w) - (by simp_all[Subst.admissible]) - (by grind[Program.bound_effect']) - have := Subst.preserve_semantics.formula σ i w Φ Φ' - grind + intro ⟨w', hw⟩ + apply Exists.intro w' + have := Subst.preserve_semantics.program σ U i v w w' hvw α α' + simp_all only [iff_true, forall_const, and_true] + have := Program.bound_effect this + rw[Program.bound_vars_decidable α'] at this + have hww' : w'.isEqExcept w V.toSet := by + grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + = Set.mem_union] + have := Subst.preserve_semantics.formula σ V i w' w hww' Φ Φ' + grind only | .ref α β => simp_all[Formula.denote, Formula.applySubst, Option.bind] split at hs @@ -929,36 +978,47 @@ theorem Subst.preserve_semantics.formula next _ _ α' _ _ _ β' _ => apply Iff.intro all_goals - intros h₁ w h₂ - have := Subst.preserve_semantics.program σ i v w α α' - have := Subst.preserve_semantics.program σ i v w β β' + intros h₁ w' h₂ + have := Subst.preserve_semantics.program σ U i v w w' hvw α α' + have := Subst.preserve_semantics.program σ U i v w w' hvw β β' grind | .applyPred p args => - simp_all[Formula.denote, Formula.applySubst, Option.bind] + simp[Formula.applySubst, Option.bind] at hs split at hs . contradiction - simp_all + simp only at hs next _ args' _ => - have : (fun (x : Fin p.arity) => Term.denote (σ.adjoint i v) v args.toVector[↑(x : ℕ)]) + have : (fun (x : Fin p.arity) => Term.denote (σ.adjoint i w) v args.toVector[↑(x : ℕ)]) = (fun (x : Fin p.arity) => Term.denote i v args'.toVector[↑x]) := by funext x apply Eq.symm - apply Subst.preserve_semantics.term _ ∅ _ _ _ (Set.eqOn_refl _ _) + apply Subst.preserve_semantics.term _ U _ _ _ hvw apply Eq.symm apply Subst.apply_subst_term_vector_to_term assumption split at hs - . + . split at hs + . contradiction + simp_all -- we do apply the subst - apply Subst.preserve_semantics.formula (σ := args'.toSubst) (v := v) (i := i) at hs - rw[hs] - rw[subst_adjoint_of_term_vector_to_subst] - simp_all[Subst.adjoint] + apply Subst.preserve_semantics.formula args'.toSubst ∅ i v v at hs + . + rw[hs] + rw[subst_adjoint_of_term_vector_to_subst] + simp[Formula.denote, adjoint] + rw[this] + apply Iff.intro + all_goals + apply Formula.coincidence + simp_all[State.isEqExcept, ←Set.disjoint_iff_inter_eq_empty] + grind only [Formula.free_vars_decidable, = Set.disjoint_left, Set.EqOn, = Set.mem_compl_iff] + . + simp_all only [State.isEqExcept, FCSet.to_set_empty, Set.compl_empty, Set.eqOn_univ] . -- we dont apply the subst - have := @Subst.adjoint_noeffect_nomem_pred i v p σ (by assumption) + have := @Subst.adjoint_noeffect_nomem_pred i w p σ (by assumption) simp_all[Formula.denote, Subst.adjoint] termination_by (σ.size, Φ.size) decreasing_by @@ -977,11 +1037,13 @@ decreasing_by theorem Subst.preserve_semantics.program (σ : Subst) + (U : FCSet Assignable) (i : Interpretation) - (v w : State) + (v v' w : State) + (hvv' : v.isEqExcept v' U) (α α' : Program) - (hs : α' = Program.applySubst σ α) - : ⟨v, w⟩ ∈ Program.denote i α' ↔ ⟨v, w⟩ ∈ Program.denote (Subst.adjoint σ i v) α := by + (hs : α' = Program.applySubst σ U α) + : ⟨v, w⟩ ∈ Program.denote i α' ↔ ⟨v, w⟩ ∈ Program.denote (Subst.adjoint σ i v') α := by match α with | .const a => simp_all[Program.denote, Program.applySubst, Subst.adjoint] @@ -991,7 +1053,7 @@ theorem Subst.preserve_semantics.program . contradiction rename Term => t' simp_all[Program.denote] - have := Subst.preserve_semantics.term σ ∅ i v _ (Set.eqOn_refl _ _) t t' + have := Subst.preserve_semantics.term σ U i v _ hvv' t t' grind | .random x => simp[Program.applySubst] at hs @@ -1003,7 +1065,7 @@ theorem Subst.preserve_semantics.program . contradiction rename Formula => Φ' simp_all[Program.denote] - have := Subst.preserve_semantics.formula σ i v Φ Φ' + have := Subst.preserve_semantics.formula σ U i v _ hvv' Φ Φ' grind | .choice α β => simp_all[Program.denote, Program.applySubst, Option.bind] @@ -1014,118 +1076,78 @@ theorem Subst.preserve_semantics.program . contradiction simp_all[Program.denote] next _ _ _ α' _ _ _ β' _ => - have := Subst.preserve_semantics.program σ i v w α α' - have := Subst.preserve_semantics.program σ i v w β β' + have := Subst.preserve_semantics.program σ U i v _ w hvv' α α' + have := Subst.preserve_semantics.program σ U i v _ w hvv' β β' grind | .seq α β => - simp_all[Program.denote, Program.applySubst, Option.bind] - split at hs - . contradiction - simp_all + simp[Program.applySubst, Option.bind] at hs split at hs . contradiction + simp only at hs split at hs . contradiction simp_all[Program.denote] - next α' _ _ _ _ _ _ β' _ _ => + next α' _ _ _ β' _ => + set V := α'.boundVars' ∪ U apply Iff.intro - . - intros h - obtain ⟨w', hw'⟩ := h - apply Exists.intro w' - and_intros - . - have := Subst.preserve_semantics.program σ i v w' α α' - grind - . - have := Subst.preserve_semantics.program σ i w' w β β' - have := Subst.admissible_adjoint.program (U := α'.boundVars') - (α := β) (i := i) - (σ := σ) (v := v) (w := w') - (by simp_all[Subst.admissible]) - (by grind[Program.bound_effect']) - - grind - . - intros h - obtain ⟨w', hw'⟩ := h + all_goals + intro ⟨w', hw'⟩ apply Exists.intro w' - and_intros - . - have := Subst.preserve_semantics.program σ i v w' α α' - grind - . - have := Subst.preserve_semantics.program σ i v w' α α' - have := Subst.preserve_semantics.program σ i w' w β β' - have := Subst.admissible_adjoint.program (U := α'.boundVars') - (α := β) (i := i) - (σ := σ) (v := v) (w := w') - (by simp_all[Subst.admissible]) - (by grind[Program.bound_effect']) - - grind + have := Subst.preserve_semantics.program σ U i v _ w' hvv' α α' + simp_all only [iff_true, forall_const, true_and] + have := Program.bound_effect this + rw[Program.bound_vars_decidable α'] at this + have hw'v' : w'.isEqExcept v' V.toSet := by + grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + = Set.mem_union] + have := Subst.preserve_semantics.program σ V i w' _ w hw'v' β β' + grind only | .loop α => - simp_all[Program.denote, Program.applySubst, Option.bind] + simp[Program.applySubst, Option.bind] at hs split at hs . contradiction - simp_all + -- first pass to get bound variables + simp at hs + rename Program => α' + have := Subst.preserve_semantics.program σ U i v _ w hvv' α α' + set V := α'.boundVars' ∪ U split at hs . contradiction - rename Program => α' + rename Program => α'' + have : α'' = α' := by grind only [Program.applySubst_unique] + simp_all[Program.denote] - have := Subst.preserve_semantics.program σ i v w α α' apply Iff.intro - . + all_goals intros h induction h with | rfl => grind[LoopClosure] - | trans v w h₁ h₂ ih => - have := ih (by apply Subst.preserve_semantics.program) - apply LoopClosure.trans (v := v) + | trans v₂ w h₁ h₂ ih => + have := ih (by apply Subst.preserve_semantics.program _ _ _ _ _ _ hvv'; simp_all only) + apply LoopClosure.trans (v := v₂) . grind . - next u _ _ _ _ _ _ _ _ _ _ _ => - have := (Subst.preserve_semantics.program σ i v w α α' (by grind)).mp h₂ - have := Subst.admissible_adjoint.program (U := α'.boundVars') (α := α) (i := i) - (σ := σ) (v := u) (w := v) - (by simp_all[Subst.admissible]) - (by grind) - - simp_all[Membership.mem, Set.Mem] - . - intros h - induction h with - | rfl => grind[LoopClosure] - | trans v w h₁ h₂ ih => - have := ih (by apply Subst.preserve_semantics.program) - apply LoopClosure.trans (v := v) - . grind - . - next u _ _ _ _ _ _ _ _ _ _ _ => - have := Subst.admissible_adjoint.program (U := α'.boundVars') (α := α) (i := i) - (σ := σ) (v := u) (w := v) - (by simp_all[Subst.admissible]) - (by grind) - - have := (Subst.preserve_semantics.program σ i v w α α' (by grind)).mpr - (by rw[← this] ; exact h₂) - - simp_all[Membership.mem, Set.Mem] + have := @Program.bound_effect α'.loop v v₂ i + rw[Program.bound_vars_decidable α'.loop] at this + simp_all[Program.denote, Program.boundVars'] + have hv₂v' : v₂.isEqExcept v' V.toSet := by + grind only [!FCSet.to_set_union, State.isEqExcept, Set.EqOn, + = Set.mem_compl_iff, = Set.mem_union] + have := Subst.preserve_semantics.program σ V i v₂ v' w hv₂v' α α' + simp_all[V,Membership.mem, Set.Mem] | .ode system Ψ => simp[Program.applySubst, Option.bind] at hs split at hs . contradiction - simp_all + simp only at hs split at hs . contradiction simp_all - split at hs - . contradiction - simp_all - split at hs - . contradiction rename List ODE => ssystem rename Formula => Ψ' + let vars := (system.map ODE.var).toFinset + let vars' := vars.map Assignable.diff_emb + set V := (.Finite (vars ∪ vars')) ∪ U simp_all[Program.denote] have hassign : OdeSystem.assignables ssystem = OdeSystem.assignables system := @@ -1133,7 +1155,8 @@ theorem Subst.preserve_semantics.program rw[hassign] apply Iff.intro - . rintro ⟨r, hr, φ, heq0, heqr, hflow⟩ + all_goals + rintro ⟨r, hr, φ, heq0, heqr, hflow⟩ apply Exists.intro r and_intros . grind @@ -1149,66 +1172,17 @@ theorem Subst.preserve_semantics.program have := hflow ζ h₁ h₂ have := ode_evolution_formula_applySubst - (σ := σ) (system := system) (ssystem := ssystem) + (σ := σ) (U := V) (system := system) (ssystem := ssystem) (Ψ := Ψ) (Ψ' := Ψ') (by grind) (by grind) - have := Subst.preserve_semantics.formula σ i (φ ζ) + have hφv' : (φ ζ).isEqExcept v' V.toSet := by + specialize hflow ζ h₁ h₂ + clear * - hvv' heq0 hflow + grind[State.isEqExcept, Set.EqOn, OdeSystem.assignables] + have := Subst.preserve_semantics.formula σ V i (φ ζ) v' hφv' (odeEvolutionFormula system Ψ) (odeEvolutionFormula ssystem Ψ') (by grind) - - have := this.mp (by grind) - - have := ode_evolution_formula_admissible σ system Ψ - (.Finite (system.assignables ∪ system.assignables.map Assignable.diff_emb)) - (by simp_all[Subst.admissible, OdeSystem.assignables]) - (by simp_all[Subst.admissible, OdeSystem.assignables]) - - have := Subst.admissible_adjoint.formula - (v := v) (w := φ ζ) (σ := σ) - (i := i) (Φ := odeEvolutionFormula system Ψ) - (U := .Finite (system.assignables ∪ system.assignables.map Assignable.diff_emb)) - (by simp_all [Subst.admissible]) - (by simp_all[State.isEqOn, State.isEqExcept, Set.EqOn]) - - grind - . grind - . grind - . rintro ⟨r, hr, φ, heq0, heqr, hflow⟩ - apply Exists.intro r - and_intros - . grind - . - apply Exists.intro φ - and_intros - . grind - . grind - . - intros ζ h₁ h₂ - and_intros - . - have := hflow ζ h₁ h₂ - - have := ode_evolution_formula_applySubst - (σ := σ) (system := system) (ssystem := ssystem) - (Ψ := Ψ) (Ψ' := Ψ') (by grind) (by grind) - - have := Subst.preserve_semantics.formula σ i (φ ζ) - (odeEvolutionFormula system Ψ) - (odeEvolutionFormula ssystem Ψ') (by grind) - - have := ode_evolution_formula_admissible σ system Ψ - (.Finite (system.assignables ∪ system.assignables.map Assignable.diff_emb)) - (by simp_all[Subst.admissible, OdeSystem.assignables]) - (by simp_all[Subst.admissible, OdeSystem.assignables]) - - have := Subst.admissible_adjoint.formula - (v := v) (w := φ ζ) (σ := σ) - (i := i) (Φ := odeEvolutionFormula system Ψ) - (U := .Finite (system.assignables ∪ system.assignables.map Assignable.diff_emb)) - (by simp_all [Subst.admissible]) - (by simp_all [State.isEqOn, State.isEqExcept, Set.EqOn]) - - grind + grind only . grind . grind termination_by (σ.size, α.size) @@ -1220,35 +1194,30 @@ end -- Uniform Substitution for Differential Dynamic Logic is sound! theorem US {σ : Subst} {Φ Φ' : Formula} - : Formula.applySubst σ Φ = Φ' + : Formula.applySubst σ ∅ Φ = Φ' → (∀ (i : Interpretation) (v : State), v ∈ Formula.denote i Φ) → (∀ (i : Interpretation) (v : State), v ∈ Formula.denote i Φ') := by intros h₁ h₂ i v have := h₂ i v - have := Subst.preserve_semantics.formula σ i v Φ Φ' (by grind) + have := Subst.preserve_semantics.formula σ ∅ i v v (Set.eqOn_refl _ _) Φ Φ' (by grind) simp_all theorem US_rule {σ : Subst} (premises : List (Formula × Formula)) (Ψ Ψ' : Formula) - (hp : ∀ Φ ∈ premises, Formula.applySubst σ Φ.1 = Φ.2) - (hΨ : Formula.applySubst σ Ψ = Ψ') - (hσ : Subst.freeVars σ .none = ∅) + (hp : ∀ Φ ∈ premises, Formula.applySubst σ .univ Φ.1 = Φ.2) + (hΨ : Formula.applySubst σ .univ Ψ = Ψ') : (∀ (i : Interpretation), (∀ (v : State) (Φ : Formula × Formula), Φ ∈ premises → v ∈ Formula.denote i Φ.1) → (∀ (v : State), v ∈ Formula.denote i Ψ)) → (∀ (i : Interpretation), (∀ (v : State) (Φ : Formula × Formula), Φ ∈ premises → v ∈ Formula.denote i Φ.2) → (∀ (v : State), v ∈ Formula.denote i Ψ')) := by intros h₁ i h₂ v - have := by - apply h₁ (Subst.adjoint σ i v) (?_) v + have : ∀ (w : State), ∀ Φ ∈ premises, w ∈ Formula.denote (σ.adjoint i v) Φ.1:= by intros w Φ hp - have := Subst.preserve_semantics.formula σ i w Φ.1 Φ.2 (by grind) - have := Subst.freeVars_symbol_subset_none (σ := σ) (S := (Φ.1).signature) - have := Subst.admissible_adjoint.formula - (Φ := Φ.1) (i := i) (σ := σ) - (v := v) (w := w) (U := .univ) - (by simp_all [Subst.admissible]) - (by simp_all) - grind + have := Subst.preserve_semantics.formula σ .univ i w v (by grind[State.isEqExcept, Set.EqOn]) Φ.1 Φ.2 (by grind only) + grind only - have := Subst.preserve_semantics.formula σ i v Ψ Ψ' (by grind) - grind + have : v ∈ Formula.denote (σ.adjoint i v) Ψ := + h₁ (Subst.adjoint σ i v) this v + + have := Subst.preserve_semantics.formula σ .univ i v v (Set.eqOn_refl _ _) Ψ Ψ' (by grind) + grind only diff --git a/DLean/USubst/Subst.lean b/DLean/USubst/Subst.lean index e1a0815..41c3a8d 100644 --- a/DLean/USubst/Subst.lean +++ b/DLean/USubst/Subst.lean @@ -255,35 +255,32 @@ end mutual -def Formula.applySubst (σ : Subst) (Φ : Formula) : Option Formula := match Φ with +def Formula.applySubst (σ : Subst) (U : FCSet Assignable) (Φ : Formula) : Option Formula := match Φ with | .True | .False => Φ - | .eq t₁ t₂ => do return .eq (← t₁.applySubst σ ∅) (← t₂.applySubst σ ∅) - | .gte t₁ t₂ => do return .gte (← t₁.applySubst σ ∅) (← t₂.applySubst σ ∅) - | .not Φ' => do return .not (← Φ'.applySubst σ) - | .and Φ₁ Φ₂ => do return .and (← Φ₁.applySubst σ) (← Φ₂.applySubst σ) + | .eq t₁ t₂ => do return .eq (← t₁.applySubst σ U) (← t₂.applySubst σ U) + | .gte t₁ t₂ => do return .gte (← t₁.applySubst σ U) (← t₂.applySubst σ U) + | .not Φ' => do return .not (← Φ'.applySubst σ U) + | .and Φ₁ Φ₂ => do return .and (← Φ₁.applySubst σ U) (← Φ₂.applySubst σ U) | .forall x Φ => do - guard <| σ.admissible {.var x} Φ.signature - return .forall x (← Φ.applySubst σ) + return .forall x (← Φ.applySubst σ ({.var x} ∪ U)) | .exists x Φ => do - guard <| σ.admissible {.var x} Φ.signature - return .exists x (← Φ.applySubst σ) + return .exists x (← Φ.applySubst σ ({.var x} ∪ U)) | .diamond α Φ => do - let σα ← α.applySubst σ - - guard <| σ.admissible σα.boundVars' Φ.signature - return .diamond σα (← Φ.applySubst σ) + let σα ← α.applySubst σ U + let V := σα.boundVars' ∪ U + return .diamond σα (← Φ.applySubst σ V) | .box α Φ => do - let σα ← α.applySubst σ - - guard <| σ.admissible σα.boundVars' Φ.signature - return .box (← α.applySubst σ) (← Φ.applySubst σ) + let σα ← α.applySubst σ U + let V := σα.boundVars' ∪ U + return .box σα (← Φ.applySubst σ V) | .ref α β => do - return .ref (← α.applySubst σ) (← β.applySubst σ) + return .ref (← α.applySubst σ U) (← β.applySubst σ U) | .applyPred p args => do - let sargs ← TermVector.applySubst σ ∅ args + let sargs ← TermVector.applySubst σ U args if (.Predicate p) ∈ σ then - Formula.applySubst (sargs.toSubst) (Subst.get σ p) + guard <| (Subst.get σ p).freeVars' ∩ U = ∅ + Formula.applySubst (sargs.toSubst) ∅ (Subst.get σ p) else return .applyPred p sargs termination_by (σ.size, Φ.size) @@ -294,32 +291,28 @@ next hin => apply Subst.symbol_size at hin grind only [= Prod.lex_def] -def Program.applySubst (σ : Subst) (α : Program) : Option Program := match α with - | .assign x t => return .assign x (← t.applySubst σ ∅) +def Program.applySubst (σ : Subst) (U : FCSet Assignable) (α : Program) : Option Program := match α with + | .assign x t => return .assign x (← t.applySubst σ U) | .random x => return .random x - | .test Φ => return .test (← Φ.applySubst σ) + | .test Φ => return .test (← Φ.applySubst σ U) | .ode system Ψ => do let vars := (system.map ODE.var).toFinset let vars' := vars.map Assignable.diff_emb - let terms := system.map ODE.term - let σΨ ← Ψ.applySubst σ - - guard <| σ.admissible (.Finite (vars ∪ vars')) Ψ.signature - guard <| terms.all (σ.admissible (.Finite (vars ∪ vars')) ∘ Term.signature) + let V := (.Finite (vars ∪ vars')) ∪ U + let σΨ ← Ψ.applySubst σ V - let ssystem ← system.mapM (fun {var, term} => do return ODE.mk var (← Term.applySubst σ ∅ term)) + let ssystem ← system.mapM (fun {var, term} => do return ODE.mk var (← Term.applySubst σ V term)) return .ode ssystem σΨ - | .choice α β => return .choice (← α.applySubst σ) (← β.applySubst σ) + | .choice α β => return .choice (← α.applySubst σ U) (← β.applySubst σ U) | .seq α β => do - let σα ← α.applySubst σ - - guard <| σ.admissible σα.boundVars' β.signature - return .seq σα (← β.applySubst σ) + let σα ← α.applySubst σ U + let V := σα.boundVars' ∪ U + return .seq σα (← β.applySubst σ V) | .loop α => do - let σα ← α.applySubst σ - - guard <| σ.admissible σα.boundVars' α.signature - return .loop σα + let σα ← α.applySubst σ U + let V := σα.boundVars' ∪ U + let σα' ← α.applySubst σ V + return .loop σα' | .const a => return Subst.get σ a termination_by (σ.size, α.size) decreasing_by @@ -884,4 +877,158 @@ decreasing_by end +/- Proof that applySubst's output does not on the taboo, as long as it does not clash. -/ +mutual + +lemma TermVector.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {n : ℕ} {ts ts₁ ts₂ : TermVector n} : + ts.applySubst σ U = ts₁ → ts.applySubst σ V = ts₂ → ts₁ = ts₂ := by + match n with + | 0 => match ts with + | .nil => + simp_all[TermVector.applySubst] + | n+1 => match ts with + | .cons t ts' => + simp_all[TermVector.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Term.applySubst_unique h₁ h₂ + have := TermVector.applySubst_unique h₁' h₂' + grind only + +lemma Term.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {t t₁ t₂ : Term} : + t.applySubst σ U = t₁ → t.applySubst σ V = t₂ → t₁ = t₂ := by + match t with + | .var _ + | .applyFn (Fn.num _) _ + | .differential _ => + grind only [Term.applySubst] + | .neg _ => + simp[Term.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ _ h₂ + have := Term.applySubst_unique h₁ h₂ + grind only + | .plus _ _ + | .times _ _ => + simp[Term.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Term.applySubst_unique h₁ h₂ + have := Term.applySubst_unique h₁' h₂' + grind only + | .applyFn (Fn.sym _) _ => + simp[Term.applySubst, Option.bind_eq_some_iff] + intro _ hθ₁ h₁ _ hθ₂ h₂ + have := TermVector.applySubst_unique hθ₁ hθ₂ + rw[this] at h₁ + split at h₁ + . simp_all[Option.bind] + split at h₁ + . contradiction + split at h₂ + . contradiction + simp_all + . simp_all +end + +lemma ode_mapM_applySubst_unique {σ : Subst} {U V : FCSet Assignable} {sys sys₁ sys₂ : OdeSystem} : + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some sys₁ → + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ V x.term)) = some sys₂ → + sys₁ = sys₂ := by + match sys with + | .nil => + simp_all + | .cons _ _ => + simp_all[Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Term.applySubst_unique h₁ h₂ + have := ode_mapM_applySubst_unique h₁' h₂' + grind only + +mutual +lemma Formula.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {φ ψ₁ ψ₂ : Formula} : + φ.applySubst σ U = ψ₁ → φ.applySubst σ V = ψ₂ → ψ₁ = ψ₂ := by + match φ with + | .True + | .False => + grind only [Formula.applySubst] + | .gte _ _ + | .eq _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Term.applySubst_unique h₁ h₂ + have := Term.applySubst_unique h₁' h₂' + grind only + | .not _ + | .exists _ _ + | .forall _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ _ h₂ + have := Formula.applySubst_unique h₁ h₂ + grind only + | .and _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Formula.applySubst_unique h₁ h₂ + have := Formula.applySubst_unique h₁' h₂' + grind only + | .box _ _ + | .diamond _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Program.applySubst_unique h₁ h₂ + have := Formula.applySubst_unique h₁' h₂' + grind only + | .ref _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Program.applySubst_unique h₁ h₂ + have := Program.applySubst_unique h₁' h₂' + grind only + | .applyPred _ _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro _ hθ₁ h₁ _ hθ₂ h₂ + have := TermVector.applySubst_unique hθ₁ hθ₂ + rw[this] at h₁ + split at h₁ + . simp_all[Option.bind] + split at h₁ + . contradiction + split at h₂ + . contradiction + simp_all + . simp_all + +lemma Program.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {α β₁ β₂ : Program} : + α.applySubst σ U = β₁ → α.applySubst σ V = β₂ → β₁ = β₂ := by + match α with + | .const _ + | .random _ => + grind only [Program.applySubst] + | .test _ => + simp[Program.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ _ h₂ + have := Formula.applySubst_unique h₁ h₂ + grind only + | .assign _ _ => + simp[Program.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ _ h₂ + have := Term.applySubst_unique h₁ h₂ + grind only + | .seq _ _ + | .choice _ _ => + simp[Program.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Program.applySubst_unique h₁ h₂ + have := Program.applySubst_unique h₁' h₂' + grind only + | .loop _ => + simp[Program.applySubst, Option.bind_eq_some_iff] + intro _ _ _ h₁' _ _ _ _ h₂' + have := Program.applySubst_unique h₁' h₂' + grind only + | .ode _ _ => + simp[Program.applySubst, Option.bind_eq_some_iff] + intro _ h₁ _ h₁' _ _ h₂ _ h₂' + have := Formula.applySubst_unique h₁ h₂ + have := ode_mapM_applySubst_unique h₁' h₂' + grind only +end end Theorems From ac044fd497d86ba2e0e40a8713be5636905da984 Mon Sep 17 00:00:00 2001 From: "E. Prebet" Date: Mon, 22 Jun 2026 15:43:16 +0200 Subject: [PATCH 3/3] feat(USubst): Efficient One-pass --- DLean/USubst/Semantics.lean | 190 ++++++------------ DLean/USubst/Subst.lean | 373 ++++++++++++++++++++++++++---------- 2 files changed, 328 insertions(+), 235 deletions(-) diff --git a/DLean/USubst/Semantics.lean b/DLean/USubst/Semantics.lean index 857bdd2..c630ad6 100644 --- a/DLean/USubst/Semantics.lean +++ b/DLean/USubst/Semantics.lean @@ -700,19 +700,6 @@ decreasing_by grind -lemma ode_mapM_assignables_eq - {σ : Subst} - {U : FCSet Assignable} - {system : OdeSystem} - {ssystem : OdeSystem} - (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) - = some ssystem) - : OdeSystem.assignables ssystem = OdeSystem.assignables system := by - unfold OdeSystem.assignables at *; - induction system generalizing ssystem <;> simp_all +decide [ List.mapM_cons ]; - cases h' : Term.applySubst σ U ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; - aesop - lemma ode_evolution_formula_applySubst {σ : Subst} {U : FCSet Assignable} @@ -760,76 +747,17 @@ lemma ode_evolution_formula_admissible unfold Subst.admissible; aesop; exact h_foldr system hterms -lemma Program.boundVars_applySubst_subset +/- Taboo set computation -/ +theorem Program.boundVars_applySubst_subset (σ : Subst) - (U : FCSet Assignable) + (U V : FCSet Assignable) (α α' : Program) : - Program.applySubst σ U α = α' → α'.boundVars ⊆ α.boundVars := by + Program.applySubst σ U α = some ⟨V,α'⟩ → α'.boundVars ∪ U ⊆ V := by intro h - match α with - | .const a => - simp[Program.boundVars] - | .test _ => - simp[Program.applySubst, Option.bind] at h - split at h - . contradiction - simp at h - rw[←h] - simp[Program.boundVars] - | .assign _ _ => - simp[Program.applySubst, Option.bind] at h - split at h - . contradiction - simp at h - rw[←h] - simp[Program.boundVars] - | .random _ => - simp[Program.applySubst] at h - rw[←h] - | .choice β γ - | .seq β γ => - simp[Program.applySubst, Option.bind] at h - split at h - . contradiction - simp only at h - split at h - . contradiction - simp at h - next β' hβ _ _ γ' hγ => - apply Program.boundVars_applySubst_subset at hγ - apply Program.boundVars_applySubst_subset at hβ - grind only [= Set.subset_def, boundVars, = Set.mem_union] - | .loop β => - simp[Program.applySubst, Option.bind] at h - split at h - . contradiction - simp only at h - split at h - . contradiction - simp at h - next β' hβ => - apply Program.boundVars_applySubst_subset at hβ - grind only [boundVars] - | .ode sys _ => - simp[Program.applySubst, Option.bind] at h - split at h - . contradiction - simp only at h - split at h - . contradiction - simp at h - next sys' hsys => - have hassign : OdeSystem.assignables sys' = OdeSystem.assignables sys := - ode_mapM_assignables_eq (show _ = some sys' from ‹_›) - grind only [boundVars, = Set.subset_def] - -lemma Program.boundVars'_applySubst_subset - (σ : Subst) - (U : FCSet Assignable) - (α α' : Program) : - Program.applySubst σ U α = α' → α'.boundVars'.toSet ⊆ α.boundVars'.toSet := by - rw[←Program.bound_vars_decidable α, ←Program.bound_vars_decidable α'] - apply Program.boundVars_applySubst_subset + have := Program.substBoundVars_applySubst h + apply Program.substBoundVars_applySubst_boundVars at h + rw[Program.bound_vars_decidable α'] + grind only [= Set.subset_def, FCSet.to_set_union] set_option maxHeartbeats 0 in /- Good things take time (dunno if that is one of them) --/ @@ -926,19 +854,19 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all - rename Program => α' + rename FCSet Assignable × Program => Vα' + rcases Vα' with ⟨V,α'⟩ rename Formula => Φ' simp_all[Formula.denote] - set V := α'.boundVars' ∪ U apply Iff.intro all_goals intros h₁ w' h₂ - have := Subst.preserve_semantics.program σ U i v w w' hvw α α' + have := Subst.preserve_semantics.program σ U V i v w w' hvw α α' simp_all only [iff_true, forall_const] - have := Program.bound_effect this - rw[Program.bound_vars_decidable α'] at this have hww' : w'.isEqExcept w V.toSet := by - grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + have := Program.bound_effect this + have := Program.boundVars_applySubst_subset σ U V α α' + grind only [= Set.subset_def, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, = Set.mem_union] have := Subst.preserve_semantics.formula σ V i w' w hww' Φ Φ' grind only @@ -950,20 +878,20 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all - rename Program => α' + rename FCSet Assignable × Program => Vα' + rcases Vα' with ⟨V,α'⟩ rename Formula => Φ' simp_all[Formula.denote] - set V := α'.boundVars' ∪ U apply Iff.intro all_goals intro ⟨w', hw⟩ apply Exists.intro w' - have := Subst.preserve_semantics.program σ U i v w w' hvw α α' + have := Subst.preserve_semantics.program σ U V i v w w' hvw α α' simp_all only [iff_true, forall_const, and_true] - have := Program.bound_effect this - rw[Program.bound_vars_decidable α'] at this have hww' : w'.isEqExcept w V.toSet := by - grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + have := Program.bound_effect this + have := Program.boundVars_applySubst_subset σ U V α α' + grind only [= Set.subset_def, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, = Set.mem_union] have := Subst.preserve_semantics.formula σ V i w' w hww' Φ Φ' grind only @@ -975,12 +903,12 @@ theorem Subst.preserve_semantics.formula split at hs . contradiction simp_all[Formula.denote] - next _ _ α' _ _ _ β' _ => + next _ _ Vα' _ _ _ Wβ' _ => apply Iff.intro all_goals intros h₁ w' h₂ - have := Subst.preserve_semantics.program σ U i v w w' hvw α α' - have := Subst.preserve_semantics.program σ U i v w w' hvw β β' + have := Subst.preserve_semantics.program σ U Vα'.1 i v w w' hvw α Vα'.2 + have := Subst.preserve_semantics.program σ U Wβ'.1 i v w w' hvw β Wβ'.2 grind | .applyPred p args => simp[Formula.applySubst, Option.bind] at hs @@ -1037,12 +965,12 @@ decreasing_by theorem Subst.preserve_semantics.program (σ : Subst) - (U : FCSet Assignable) + (U V : FCSet Assignable) (i : Interpretation) (v v' w : State) (hvv' : v.isEqExcept v' U) (α α' : Program) - (hs : α' = Program.applySubst σ U α) + (hs : some ⟨V,α'⟩ = Program.applySubst σ U α) : ⟨v, w⟩ ∈ Program.denote i α' ↔ ⟨v, w⟩ ∈ Program.denote (Subst.adjoint σ i v') α := by match α with | .const a => @@ -1057,7 +985,7 @@ theorem Subst.preserve_semantics.program grind | .random x => simp[Program.applySubst] at hs - rw[hs] + rw[hs.2] simp only [Program.denote] | .test Φ => simp_all[Program.denote, Program.applySubst, Option.bind] @@ -1075,9 +1003,9 @@ theorem Subst.preserve_semantics.program split at hs . contradiction simp_all[Program.denote] - next _ _ _ α' _ _ _ β' _ => - have := Subst.preserve_semantics.program σ U i v _ w hvv' α α' - have := Subst.preserve_semantics.program σ U i v _ w hvv' β β' + next _ _ _ Vα' _ _ _ Wβ' _ => + have := Subst.preserve_semantics.program σ U Vα'.1 i v _ w hvv' α Vα'.2 + have := Subst.preserve_semantics.program σ U Wβ'.1 i v _ w hvv' β Wβ'.2 grind | .seq α β => simp[Program.applySubst, Option.bind] at hs @@ -1087,20 +1015,21 @@ theorem Subst.preserve_semantics.program split at hs . contradiction simp_all[Program.denote] - next α' _ _ _ β' _ => - set V := α'.boundVars' ∪ U + next Vα' _ _ _ Wβ' _ => + rcases Vα' with ⟨V,α'⟩ + rcases Wβ' with ⟨W,β'⟩ apply Iff.intro all_goals intro ⟨w', hw'⟩ apply Exists.intro w' - have := Subst.preserve_semantics.program σ U i v _ w' hvv' α α' + have := Subst.preserve_semantics.program σ U V i v _ w' hvv' α α' simp_all only [iff_true, forall_const, true_and] - have := Program.bound_effect this - rw[Program.bound_vars_decidable α'] at this have hw'v' : w'.isEqExcept v' V.toSet := by - grind only [FCSet.to_set_union, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, + have := Program.bound_effect this + have := Program.boundVars_applySubst_subset σ U V α α' + grind only [= Set.subset_def, State.isEqExcept, Set.EqOn, = Set.mem_compl_iff, = Set.mem_union] - have := Subst.preserve_semantics.program σ V i w' _ w hw'v' β β' + have := Subst.preserve_semantics.program σ V W i w' _ w hw'v' β β' grind only | .loop α => simp[Program.applySubst, Option.bind] at hs @@ -1108,13 +1037,10 @@ theorem Subst.preserve_semantics.program . contradiction -- first pass to get bound variables simp at hs - rename Program => α' - have := Subst.preserve_semantics.program σ U i v _ w hvv' α α' - set V := α'.boundVars' ∪ U - split at hs - . contradiction - rename Program => α'' - have : α'' = α' := by grind only [Program.applySubst_unique] + rename FCSet Assignable × Program => Vα' + rcases Vα' with ⟨V, α'⟩ + set V' := Program.substBoundVars σ α ∪ U + have := Subst.preserve_semantics.program σ U V i v _ w hvv' α α' simp_all[Program.denote] apply Iff.intro @@ -1123,18 +1049,19 @@ theorem Subst.preserve_semantics.program induction h with | rfl => grind[LoopClosure] | trans v₂ w h₁ h₂ ih => - have := ih (by apply Subst.preserve_semantics.program _ _ _ _ _ _ hvv'; simp_all only) + have := ih (by apply Subst.preserve_semantics.program _ _ _ _ _ _ _ hvv') apply LoopClosure.trans (v := v₂) - . grind + . grind only . - have := @Program.bound_effect α'.loop v v₂ i - rw[Program.bound_vars_decidable α'.loop] at this - simp_all[Program.denote, Program.boundVars'] - have hv₂v' : v₂.isEqExcept v' V.toSet := by - grind only [!FCSet.to_set_union, State.isEqExcept, Set.EqOn, - = Set.mem_compl_iff, = Set.mem_union] - have := Subst.preserve_semantics.program σ V i v₂ v' w hv₂v' α α' - simp_all[V,Membership.mem, Set.Mem] + have hv₂v' : v₂.isEqExcept v' V'.toSet := by + have := @Program.bound_effect α'.loop v v₂ i + simp_all only [Program.denote, Set.mem_setOf_eq, Program.boundVars, + forall_const] + have := Program.boundVars_applySubst_subset σ V' V α α' + have := @Program.substBoundVars_applySubst σ α α' V' V + grind[!FCSet.to_set_union, State.isEqExcept, Set.EqOn] + have := Subst.preserve_semantics.program σ V' V i v₂ v' w hv₂v' α α' + simp_all[Membership.mem, Set.Mem] | .ode system Ψ => simp[Program.applySubst, Option.bind] at hs split at hs @@ -1142,13 +1069,10 @@ theorem Subst.preserve_semantics.program simp only at hs split at hs . contradiction - simp_all + simp_all[Program.denote, -FCSet.to_set_eq] rename List ODE => ssystem rename Formula => Ψ' - let vars := (system.map ODE.var).toFinset - let vars' := vars.map Assignable.diff_emb - set V := (.Finite (vars ∪ vars')) ∪ U - simp_all[Program.denote] + set V' := FCSet.Finite (system.assignables ∪ Finset.map Assignable.diff_emb system.assignables) ∪ U have hassign : OdeSystem.assignables ssystem = OdeSystem.assignables system := ode_mapM_assignables_eq (show _ = some ssystem from ‹_›) @@ -1172,14 +1096,14 @@ theorem Subst.preserve_semantics.program have := hflow ζ h₁ h₂ have := ode_evolution_formula_applySubst - (σ := σ) (U := V) (system := system) (ssystem := ssystem) + (σ := σ) (U := V') (system := system) (ssystem := ssystem) (Ψ := Ψ) (Ψ' := Ψ') (by grind) (by grind) - have hφv' : (φ ζ).isEqExcept v' V.toSet := by + have hφv' : (φ ζ).isEqExcept v' V'.toSet := by specialize hflow ζ h₁ h₂ clear * - hvv' heq0 hflow grind[State.isEqExcept, Set.EqOn, OdeSystem.assignables] - have := Subst.preserve_semantics.formula σ V i (φ ζ) v' hφv' + have := Subst.preserve_semantics.formula σ V' i (φ ζ) v' hφv' (odeEvolutionFormula system Ψ) (odeEvolutionFormula ssystem Ψ') (by grind) grind only diff --git a/DLean/USubst/Subst.lean b/DLean/USubst/Subst.lean index 41c3a8d..0edafc6 100644 --- a/DLean/USubst/Subst.lean +++ b/DLean/USubst/Subst.lean @@ -253,6 +253,20 @@ next hin => end +/- Precomputes the bound variables post-substitution. + Used for substitution of loops. -/ +def Program.substBoundVars (σ : Subst) (α : Program) : FCSet Assignable := + match α with + | .const a => (σ.get a).boundVars' + | .test _ => ∅ + | .assign x _ + | .random x => {x} + | .choice α β + | .seq α β => α.substBoundVars σ ∪ β.substBoundVars σ + | .loop α => α.substBoundVars σ + | .ode _ _ => α.boundVars' + + mutual def Formula.applySubst (σ : Subst) (U : FCSet Assignable) (Φ : Formula) : Option Formula := match Φ with @@ -267,15 +281,13 @@ def Formula.applySubst (σ : Subst) (U : FCSet Assignable) (Φ : Formula) : Opti | .exists x Φ => do return .exists x (← Φ.applySubst σ ({.var x} ∪ U)) | .diamond α Φ => do - let σα ← α.applySubst σ U - let V := σα.boundVars' ∪ U + let ⟨V,σα⟩ ← α.applySubst σ U return .diamond σα (← Φ.applySubst σ V) | .box α Φ => do - let σα ← α.applySubst σ U - let V := σα.boundVars' ∪ U + let ⟨V,σα⟩ ← α.applySubst σ U return .box σα (← Φ.applySubst σ V) | .ref α β => do - return .ref (← α.applySubst σ U) (← β.applySubst σ U) + return .ref (← α.applySubst σ U).2 (← β.applySubst σ U).2 | .applyPred p args => do let sargs ← TermVector.applySubst σ U args if (.Predicate p) ∈ σ then @@ -291,29 +303,33 @@ next hin => apply Subst.symbol_size at hin grind only [= Prod.lex_def] -def Program.applySubst (σ : Subst) (U : FCSet Assignable) (α : Program) : Option Program := match α with - | .assign x t => return .assign x (← t.applySubst σ U) - | .random x => return .random x - | .test Φ => return .test (← Φ.applySubst σ U) +def Program.applySubst (σ : Subst) (U : FCSet Assignable) (α : Program) : Option (FCSet Assignable × Program) := match α with + | .assign x t => return ⟨{x} ∪ U, .assign x (← t.applySubst σ U)⟩ + | .random x => return ⟨{x} ∪ U, .random x⟩ + | .test Φ => return ⟨U, .test (← Φ.applySubst σ U)⟩ | .ode system Ψ => do - let vars := (system.map ODE.var).toFinset + let vars := system.assignables let vars' := vars.map Assignable.diff_emb let V := (.Finite (vars ∪ vars')) ∪ U let σΨ ← Ψ.applySubst σ V let ssystem ← system.mapM (fun {var, term} => do return ODE.mk var (← Term.applySubst σ V term)) - return .ode ssystem σΨ - | .choice α β => return .choice (← α.applySubst σ U) (← β.applySubst σ U) + return ⟨V, .ode ssystem σΨ⟩ + | .choice α β => do + let ⟨V, σα⟩ ← α.applySubst σ U + let ⟨W, σβ⟩ ← β.applySubst σ U + return ⟨V ∪ W, .choice σα σβ⟩ | .seq α β => do - let σα ← α.applySubst σ U - let V := σα.boundVars' ∪ U - return .seq σα (← β.applySubst σ V) + let ⟨V, σα⟩ ← α.applySubst σ U + let ⟨W, σβ⟩ ← β.applySubst σ V + return ⟨W, .seq σα σβ⟩ | .loop α => do - let σα ← α.applySubst σ U - let V := σα.boundVars' ∪ U - let σα' ← α.applySubst σ V - return .loop σα' - | .const a => return Subst.get σ a + let V := α.substBoundVars σ ∪ U + let ⟨W,σα⟩ ← α.applySubst σ V + return ⟨W, .loop σα⟩ + | .const a => + let σα := Subst.get σ a + return ⟨σα.boundVars' ∪ U, σα⟩ termination_by (σ.size, α.size) decreasing_by all_goals (simp_all[Program.size] ; grind) @@ -877,11 +893,74 @@ decreasing_by end -/- Proof that applySubst's output does not on the taboo, as long as it does not clash. -/ +/- Substitution preserves ode's assignables -/ +lemma ode_mapM_assignables_eq + {σ : Subst} + {U : FCSet Assignable} + {system : OdeSystem} + {ssystem : OdeSystem} + (h : system.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) + = some ssystem) + : OdeSystem.assignables ssystem = OdeSystem.assignables system := by + unfold OdeSystem.assignables at *; + induction system generalizing ssystem <;> simp_all +decide [ List.mapM_cons ]; + cases h' : Term.applySubst σ U ‹ODE›.term <;> simp_all +decide [ Option.bind_eq_some_iff ]; + aesop + +/- `Program.substBoundVars` computes the bound variables of the substituted program -/ +lemma Program.substBoundVars_applySubst_boundVars + (σ : Subst) + (U V : FCSet Assignable) + (α α' : Program) : + Program.applySubst σ U α = some ⟨V,α'⟩ → α'.boundVars' = α.substBoundVars σ := by + intro h + match α with + | .const _ + | .test _ + | .assign _ _ + | .random _ => + simp[Program.applySubst, Option.bind] at h + grind only [substBoundVars, boundVars'] + | .choice β γ + | .seq β γ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp only at h + split at h + . contradiction + simp at h + next β' hβ _ _ γ' hγ => + apply Program.substBoundVars_applySubst_boundVars at hγ + apply Program.substBoundVars_applySubst_boundVars at hβ + grind only [substBoundVars, boundVars', = Set.subset_def, = Set.mem_union] + | .loop β => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp at h + next β' hβ => + apply Program.substBoundVars_applySubst_boundVars at hβ + grind only [substBoundVars, boundVars', = Set.subset_def, = Set.mem_union] + | .ode sys _ => + simp[Program.applySubst, Option.bind] at h + split at h + . contradiction + simp only at h + split at h + . contradiction + simp at h + next sys' hsys => + have hassign : OdeSystem.assignables sys' = OdeSystem.assignables sys := + ode_mapM_assignables_eq (show _ = some sys' from ‹_›) + grind only [substBoundVars, boundVars', FCSet.to_set_eq, = Set.subset_def, = Set.mem_union, = Finset.mem_coe, + = Set.mem_image, = Finset.mem_map] + +/- Weakening the taboo does not create clash. -/ mutual -lemma TermVector.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {n : ℕ} {ts ts₁ ts₂ : TermVector n} : - ts.applySubst σ U = ts₁ → ts.applySubst σ V = ts₂ → ts₁ = ts₂ := by +lemma TermVector.taboo_mono {σ : Subst} {U V : FCSet Assignable} {n : ℕ} {ts ts' : TermVector n} : + V.toSet ⊆ U.toSet → ts.applySubst σ U = ts' → ts.applySubst σ V = ts' := by match n with | 0 => match ts with | .nil => @@ -889,13 +968,13 @@ lemma TermVector.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {n : | n+1 => match ts with | .cons t ts' => simp_all[TermVector.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Term.applySubst_unique h₁ h₂ - have := TermVector.applySubst_unique h₁' h₂' + intro hUV _ h₁ _ h₂ + have := Term.taboo_mono hUV h₁ + have := TermVector.taboo_mono hUV h₂ grind only -lemma Term.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {t t₁ t₂ : Term} : - t.applySubst σ U = t₁ → t.applySubst σ V = t₂ → t₁ = t₂ := by +lemma Term.taboo_mono {σ : Subst} {U V : FCSet Assignable} {t t' : Term} : + V.toSet ⊆ U.toSet → t.applySubst σ U = t' → t.applySubst σ V = t' := by match t with | .var _ | .applyFn (Fn.num _) _ @@ -903,48 +982,50 @@ lemma Term.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {t t₁ t₂ grind only [Term.applySubst] | .neg _ => simp[Term.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ _ h₂ - have := Term.applySubst_unique h₁ h₂ + intro hUV _ h + have := Term.taboo_mono hUV h grind only | .plus _ _ | .times _ _ => simp[Term.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Term.applySubst_unique h₁ h₂ - have := Term.applySubst_unique h₁' h₂' + intro hUV _ h₁ _ h₂ + have := Term.taboo_mono hUV h₁ + have := Term.taboo_mono hUV h₂ grind only | .applyFn (Fn.sym _) _ => simp[Term.applySubst, Option.bind_eq_some_iff] - intro _ hθ₁ h₁ _ hθ₂ h₂ - have := TermVector.applySubst_unique hθ₁ hθ₂ - rw[this] at h₁ - split at h₁ + intro hUV _ h₁ h₂ + apply TermVector.taboo_mono hUV at h₁ + split at h₂ . simp_all[Option.bind] - split at h₁ - . contradiction split at h₂ . contradiction simp_all + suffices (↑(Term.freeVars (σ.get (Symbol.Function _))) ∩ V.toSet = ∅) by + rw[this] + simp + grind only [= Set.subset_def, = Set.mem_inter_iff, = Set.mem_empty_iff_false] . simp_all end -lemma ode_mapM_applySubst_unique {σ : Subst} {U V : FCSet Assignable} {sys sys₁ sys₂ : OdeSystem} : - sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some sys₁ → - sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ V x.term)) = some sys₂ → - sys₁ = sys₂ := by +lemma ode_mapM_taboo_mono {σ : Subst} {U V : FCSet Assignable} {sys sys' : OdeSystem} : + V.toSet ⊆ U.toSet → + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some sys' → + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ V x.term)) = some sys' := by match sys with | .nil => simp_all | .cons _ _ => simp_all[Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Term.applySubst_unique h₁ h₂ - have := ode_mapM_applySubst_unique h₁' h₂' - grind only + intro hUV _ h₁ _ h₂ + have := Term.taboo_mono hUV h₁ + have := ode_mapM_taboo_mono hUV h₂ + simp_all only [Option.pure_def, Option.bind_eq_bind, Option.some.injEq, exists_eq_left', + implies_true] mutual -lemma Formula.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {φ ψ₁ ψ₂ : Formula} : - φ.applySubst σ U = ψ₁ → φ.applySubst σ V = ψ₂ → ψ₁ = ψ₂ := by +lemma Formula.taboo_mono {σ : Subst} {U V : FCSet Assignable} {φ ψ : Formula} : + V.toSet ⊆ U.toSet → φ.applySubst σ U = ψ → φ.applySubst σ V = ψ := by match φ with | .True | .False => @@ -952,83 +1033,171 @@ lemma Formula.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {φ ψ₁ | .gte _ _ | .eq _ _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Term.applySubst_unique h₁ h₂ - have := Term.applySubst_unique h₁' h₂' + intro hUV _ h₁ _ h₂ + have := Term.taboo_mono hUV h₁ + have := Term.taboo_mono hUV h₂ grind only - | .not _ - | .exists _ _ - | .forall _ _ => + | .not _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ _ h₂ - have := Formula.applySubst_unique h₁ h₂ + intro hUV _ h + have := Formula.taboo_mono hUV h grind only - | .and _ _ => + | .exists x _ + | .forall x _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Formula.applySubst_unique h₁ h₂ - have := Formula.applySubst_unique h₁' h₂' + intro hUV _ h + have : ({.var x} ∪ V).toSet ⊆ ({.var x} ∪ U).toSet := by + grind only [= Set.subset_def, FCSet.to_set_union, = Set.mem_union] + apply Formula.taboo_mono this at h grind only - | .box _ _ - | .diamond _ _ => + | .and _ _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Program.applySubst_unique h₁ h₂ - have := Formula.applySubst_unique h₁' h₂' + intro hUV _ h₁ _ h₂ + have := Formula.taboo_mono hUV h₁ + have := Formula.taboo_mono hUV h₂ grind only + | .box α _ + | .diamond α _ => + simp[Formula.applySubst, Option.bind_eq_some_iff] + intro hUV W _ h₁ _ h₂ + have := Program.taboo_mono hUV h₁ + have : α.substBoundVars σ ∪ U = W := by + have := Program.taboo_mono (Set.Subset.refl _) h₁ + grind only + rw[←this] at h₂ + have : (α.substBoundVars σ ∪ V).toSet ⊆ (α.substBoundVars σ ∪ U).toSet := by + grind only [= Set.subset_def, FCSet.to_set_union, = Set.mem_union] + have := Formula.taboo_mono this h₂ + grind only [FCSet.to_set_union, = Set.mem_union] | .ref _ _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Program.applySubst_unique h₁ h₂ - have := Program.applySubst_unique h₁' h₂' + intro hUV _ _ h₁ _ _ h₂ + have := Program.taboo_mono hUV h₁ + have := Program.taboo_mono hUV h₂ grind only | .applyPred _ _ => simp[Formula.applySubst, Option.bind_eq_some_iff] - intro _ hθ₁ h₁ _ hθ₂ h₂ - have := TermVector.applySubst_unique hθ₁ hθ₂ - rw[this] at h₁ - split at h₁ + intro hUV _ h₁ h + have := TermVector.taboo_mono hUV h₁ + split at h . simp_all[Option.bind] - split at h₁ - . contradiction - split at h₂ + split at h . contradiction simp_all + suffices (↑(Formula.freeVars' (σ.get (Symbol.Predicate _))) ∩ V.toSet = ∅) by + rw[this] + simp + grind only [= Set.subset_def, = Set.mem_inter_iff, = Set.mem_empty_iff_false] . simp_all -lemma Program.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {α β₁ β₂ : Program} : - α.applySubst σ U = β₁ → α.applySubst σ V = β₂ → β₁ = β₂ := by +lemma Program.taboo_mono {σ : Subst} {U V W: FCSet Assignable} {α β : Program} : + V.toSet ⊆ U.toSet → α.applySubst σ U = some ⟨W, β⟩ → α.applySubst σ V = some ⟨α.substBoundVars σ ∪ V, β⟩ := by match α with | .const _ | .random _ => - grind only [Program.applySubst] + grind only [Program.applySubst, Program.substBoundVars, = Option.pure_apply] | .test _ => - simp[Program.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ _ h₂ - have := Formula.applySubst_unique h₁ h₂ + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff] + intro hUV _ h + have := Formula.taboo_mono hUV h grind only | .assign _ _ => - simp[Program.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ _ h₂ - have := Term.applySubst_unique h₁ h₂ + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff] + intro hUV _ h + have := Term.taboo_mono hUV h grind only - | .seq _ _ | .choice _ _ => - simp[Program.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Program.applySubst_unique h₁ h₂ - have := Program.applySubst_unique h₁' h₂' - grind only - | .loop _ => - simp[Program.applySubst, Option.bind_eq_some_iff] - intro _ _ _ h₁' _ _ _ _ h₂' - have := Program.applySubst_unique h₁' h₂' - grind only - | .ode _ _ => - simp[Program.applySubst, Option.bind_eq_some_iff] - intro _ h₁ _ h₁' _ _ h₂ _ h₂' - have := Formula.applySubst_unique h₁ h₂ - have := ode_mapM_applySubst_unique h₁' h₂' - grind only + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff] + intro hUV _ _ h₁ _ _ h₂ + have := Program.taboo_mono hUV h₁ + have := Program.taboo_mono hUV h₂ + grind only [FCSet.to_set_union, = Set.mem_union] + | .seq α _ => + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff] + intro hUV W _ h₁ _ _ h₂ + have := Program.taboo_mono hUV h₁ + have : α.substBoundVars σ ∪ U = W := by + have := Program.taboo_mono (Set.Subset.refl _) h₁ + grind only + rw[←this] at h₂ + have : (α.substBoundVars σ ∪ V).toSet ⊆ (α.substBoundVars σ ∪ U).toSet := by + grind only [= Set.subset_def, FCSet.to_set_union, = Set.mem_union] + have := Program.taboo_mono this h₂ + grind only [FCSet.to_set_union, = Set.mem_union] + | .loop α => + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff] + intro hUV _ _ h₁ _ h₂ + have : (α.substBoundVars σ ∪ V).toSet ⊆ (α.substBoundVars σ ∪ U).toSet := by + grind only [= Set.subset_def, FCSet.to_set_union, = Set.mem_union] + have := Program.taboo_mono this h₁ + grind only [FCSet.to_set_union, = Set.mem_union] + | .ode sys _ => + simp[Program.applySubst, Program.substBoundVars, Option.bind_eq_some_iff, -FCSet.to_set_eq] + intro hUV _ h₁ _ h₂ + set BV := FCSet.Finite (sys.assignables ∪ Finset.map Assignable.diff_emb sys.assignables) + have hUV' : (BV ∪ V).toSet ⊆ (BV ∪ U).toSet := by + grind only [= Set.subset_def, FCSet.to_set_union, = Set.mem_union] + have := Formula.taboo_mono hUV' h₁ + have := ode_mapM_taboo_mono hUV' h₂ + simp_all[BV, Program.boundVars'] + end + +/- Corollary: USubst updated taboo coincides with `Program.substBoundVars`. -/ +theorem Program.substBoundVars_applySubst {σ : Subst} {α α' : Program} {U V : FCSet Assignable} : + α.applySubst σ U = some ⟨V, α'⟩ → α.substBoundVars σ ∪ U = V := by + intro h + have := Program.taboo_mono (Set.Subset.refl _) h + grind only + +/- Corollary: applySubst's output is unique (w.r.t the taboo), as long as it does not clash. -/ + +lemma TermVector.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {n : ℕ} {ts ts₁ ts₂ : TermVector n} : + ts.applySubst σ U = ts₁ → ts.applySubst σ V = ts₂ → ts₁ = ts₂ := by + intro h₁ h₂ + obtain ⟨hU,hV⟩ : (U ∩ V).toSet ⊆ U.toSet ∧ (U ∩ V).toSet ⊆ V.toSet := by + grind only [= Set.subset_def, FCSet.to_set_inter, = Set.mem_inter_iff] + apply TermVector.taboo_mono hU at h₁ + apply TermVector.taboo_mono hV at h₂ + grind only + +lemma Term.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {t t₁ t₂ : Term} : + t.applySubst σ U = t₁ → t.applySubst σ V = t₂ → t₁ = t₂ := by + intro h₁ h₂ + obtain ⟨hU,hV⟩ : (U ∩ V).toSet ⊆ U.toSet ∧ (U ∩ V).toSet ⊆ V.toSet := by + grind only [= Set.subset_def, FCSet.to_set_inter, = Set.mem_inter_iff] + apply Term.taboo_mono hU at h₁ + apply Term.taboo_mono hV at h₂ + grind only + + +lemma ode_mapM_applySubst_unique {σ : Subst} {U V : FCSet Assignable} {sys sys₁ sys₂ : OdeSystem} : + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ U x.term)) = some sys₁ → + sys.mapM (fun x => do return ODE.mk x.var (← Term.applySubst σ V x.term)) = some sys₂ → + sys₁ = sys₂ := by + intro h₁ h₂ + obtain ⟨hU,hV⟩ : (U ∩ V).toSet ⊆ U.toSet ∧ (U ∩ V).toSet ⊆ V.toSet := by + grind only [= Set.subset_def, FCSet.to_set_inter, = Set.mem_inter_iff] + apply ode_mapM_taboo_mono hU at h₁ + apply ode_mapM_taboo_mono hV at h₂ + grind only + +lemma Formula.applySubst_unique {σ : Subst} {U V : FCSet Assignable} {φ ψ₁ ψ₂ : Formula} : + φ.applySubst σ U = ψ₁ → φ.applySubst σ V = ψ₂ → ψ₁ = ψ₂ := by + intro h₁ h₂ + obtain ⟨hU,hV⟩ : (U ∩ V).toSet ⊆ U.toSet ∧ (U ∩ V).toSet ⊆ V.toSet := by + grind only [= Set.subset_def, FCSet.to_set_inter, = Set.mem_inter_iff] + apply Formula.taboo_mono hU at h₁ + apply Formula.taboo_mono hV at h₂ + grind only + +lemma Program.applySubst_unique {σ : Subst} {U V W₁ W₂ : FCSet Assignable} {α β₁ β₂ : Program} : + α.applySubst σ U = some ⟨W₁, β₁⟩ → α.applySubst σ V = some ⟨W₂, β₂⟩ → β₁ = β₂ := by + intro h₁ h₂ + obtain ⟨hU,hV⟩ : (U ∩ V).toSet ⊆ U.toSet ∧ (U ∩ V).toSet ⊆ V.toSet := by + grind only [= Set.subset_def, FCSet.to_set_inter, = Set.mem_inter_iff] + apply Program.taboo_mono hU at h₁ + apply Program.taboo_mono hV at h₂ + grind only + end Theorems