From 5249b548b91b6092dca2e849290e21a24449ed6f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 13 Jan 2025 18:40:45 +0100 Subject: [PATCH] Approx & its monotonicity --- Juvix/Core/Main/Language/Value.lean | 2 +- Juvix/Core/Main/Semantics.lean | 143 ++++++++++++++++++++-------- Juvix/Utils.lean | 40 ++++++++ 3 files changed, 143 insertions(+), 42 deletions(-) create mode 100644 Juvix/Utils.lean diff --git a/Juvix/Core/Main/Language/Value.lean b/Juvix/Core/Main/Language/Value.lean index 230e512..b584946 100644 --- a/Juvix/Core/Main/Language/Value.lean +++ b/Juvix/Core/Main/Language/Value.lean @@ -4,10 +4,10 @@ import Juvix.Core.Main.Language.Base namespace Juvix.Core.Main inductive Value : Type where + | unit : Value | const : Constant → Value | constr_app : (constr : Name) → (args_rev : List Value) → Value | closure : (ctx : List Value) → (value : Expr) → Value - | unit : Value deriving Inhabited abbrev Context : Type := List Value diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean index cb22bdd..36f0e6a 100644 --- a/Juvix/Core/Main/Semantics.lean +++ b/Juvix/Core/Main/Semantics.lean @@ -1,6 +1,8 @@ import Juvix.Core.Main.Language import Mathlib.Tactic.CC +import Juvix.Utils +import Aesop namespace Juvix.Core.Main @@ -106,33 +108,110 @@ theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : ⟨P⟩ ctx ⊢ e ↦ v cases h₂ <;> cc mutual - inductive Value.Equiv (P : Program) : Value → Value → Prop where - | const {c} : Value.Equiv P (Value.const c) (Value.const c) - | constr_app {ctr_name args_rev args_rev'} : - (∀ p ∈ List.zip args_rev args_rev', Value.Equiv P (Prod.fst p) (Prod.snd p)) → - Value.Equiv P (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev') - | closure {ctx₁ body₁ ctx₂ body₂} : - (∀ v v', ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v' → Expr.EvalsToEquiv P (v :: ctx₂) body₂ v') → - (∀ v v', ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦ v' → Expr.EvalsToEquiv P (v :: ctx₁) body₁ v') → - Value.Equiv P (Value.closure ctx₁ body₁) (Value.closure ctx₂ body₂) - | unit : Value.Equiv P Value.unit Value.unit - - -- We need `Expr.EvalsToEquiv` in order to avoid existential quantification in - -- the definition of `Value.Equiv`. - inductive Expr.EvalsToEquiv (P : Program) : Context → Expr → Value → Prop where - | equiv {ctx e v v'} : - ⟨P⟩ ctx ⊢ e ↦ v' → - Value.Equiv P v v' → - Expr.EvalsToEquiv P ctx e v + @[aesop unsafe [constructors, cases]] + inductive Value.Approx.Indexed (P : Program) : Nat → Value → Value → Prop where + | refl {n v} : Value.Approx.Indexed P n v v + | constr_app {n ctr_name args_rev args_rev'} : + (∀ p ∈ List.zip args_rev args_rev', Value.Approx.Indexed P n (Prod.fst p) (Prod.snd p)) → + Value.Approx.Indexed P (Nat.succ n) (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev') + | closure {n ctx₁ body₁ ctx₂ body₂} : + (∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁) → + Value.Approx.Indexed P (Nat.succ n) (Value.closure ctx₁ body₁) (Value.closure ctx₂ body₂) + + -- We need `Expr.ApproxEvals.Indexed` in order to avoid existential quantification in + -- the definition of `Value.Approx.Indexed`. + @[aesop unsafe [constructors, cases]] + inductive Expr.ApproxEvals.Indexed (P : Program) : Nat → Context → Expr → Value → Prop where + | equiv {n ctx e v₁ v₂} : + ⟨P⟩ ctx ⊢ e ↦ v₂ → + Value.Approx.Indexed P n v₂ v₁ → + Expr.ApproxEvals.Indexed P n ctx e v₁ end -notation "⟨" P "⟩ " e " ≈ " e':40 => Value.Equiv P e e' - -notation "⟨" P "⟩ " ctx " ⊢ " e " ↦≈ " v:40 => Expr.EvalsToEquiv P ctx e v +lemma Value.Approx.Indexed.monotone {P n n' v v'} (h : Value.Approx.Indexed P n v v') (h' : n ≤ n') : Value.Approx.Indexed P n' v v' := by + induction n' generalizing n v v' with + | zero => + cases h' + exact h + | succ n' ih => + cases h' + case succ.refl => + exact h + case succ.step h' => + have ih' : Indexed P n' v v' := by + apply ih + case h => + exact h + case h' => + exact h' + cases ih' + case refl => + exact Value.Approx.Indexed.refl + case constr_app n' ctr_name args_rev args_rev' ch => + aesop + case closure n' ctx₁ body₁ ctx₂ body₂ ch => + have : ∀ (v v' : Value), ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v' → Expr.ApproxEvals.Indexed P n'.succ (v :: ctx₂) body₂ v' := by + intro v v' h'' + have eh : Expr.ApproxEvals.Indexed P n' (v :: ctx₂) body₂ v' := by + apply ch + exact h'' + rcases eh with ⟨h1, h2⟩ + constructor + exact h1 + aesop + aesop + +def Value.Approx (P : Program) (v v' : Value) : Prop := + ∃ n, Value.Approx.Indexed P n v v' + +def Expr.ApproxEvals (P : Program) (ctx : Context) (e : Expr) (v : Value) : Prop := + ∃ n, Expr.ApproxEvals.Indexed P n ctx e v + +notation "⟨" P "⟩ " e " ≲ " e':40 => Value.Approx P e e' + +notation "⟨" P "⟩ " ctx " ⊢ " e " ↦≳ " v:40 => Expr.ApproxEvals P ctx e v + +lemma Value.Approx.refl {P v} : ⟨P⟩ v ≲ v := by + exists 0 + exact Value.Approx.Indexed.refl + +lemma Value.Approx.zip_refl {P p} {l : List Value} (h : p ∈ l.zip l) : ⟨P⟩ p.fst ≲ p.snd := by + have h : p.fst = p.snd := Utils.zip_refl_eq l p h + rewrite [h] + exact Value.Approx.refl + +lemma Value.Approx.constr_app_inv {P ctr_name args_rev args_rev'} : + ⟨P⟩ Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' → + ∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p := by + intros h p hp + rcases h with ⟨n, h⟩ + cases h + case constr_app => + constructor + aesop + case refl => + exact Value.Approx.zip_refl hp + +lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : + (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p) → + ⟨P⟩ Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' := by + intro h + have h' : ∀ p ∈ List.zip args_rev args_rev', ∃ n, Value.Approx.Indexed P n (Prod.fst p) (Prod.snd p) := by + aesop + have nh : ∃ n, ∀ p ∈ List.zip args_rev args_rev', Value.Approx.Indexed P n (Prod.fst p) (Prod.snd p) := by + apply Juvix.Utils.monotone_ex_all + aesop (add unsafe apply Value.Approx.Indexed.monotone) + assumption + obtain ⟨n, h''⟩ := nh + exists (Nat.succ n) + constructor + assumption + +def Expr.Approx (P₁ : Program) (ctx₁ : Context) (e₁ : Expr) (P₂ : Program) (ctx₂ : Context) (e₂ : Expr) : Prop := + (∀ v, ⟨P₁⟩ ctx₁ ⊢ e₁ ↦ v → ⟨P₂⟩ ctx₂ ⊢ e₂ ↦≳ v) def Expr.Equiv (P₁ : Program) (ctx₁ : Context) (e₁ : Expr) (P₂ : Program) (ctx₂ : Context) (e₂ : Expr) : Prop := - (∀ v, ⟨P₁⟩ ctx₁ ⊢ e₁ ↦ v → ⟨P₂⟩ ctx₂ ⊢ e₂ ↦≈ v) ∧ - (∀ v, ⟨P₂⟩ ctx₂ ⊢ e₂ ↦ v → ⟨P₁⟩ ctx₁ ⊢ e₁ ↦≈ v) + Expr.Approx P₁ ctx₁ e₁ P₂ ctx₂ e₂ ∧ Expr.Approx P₂ ctx₂ e₂ P₁ ctx₁ e₁ notation "⟨" P₁ "⟩ " ctx₁ " ⊢ " e₁ " ≋ " "⟨" P₂ "⟩ " ctx₂ " ⊢ " e₂:40 => Expr.Equiv P₁ ctx₁ e₁ P₂ ctx₂ e₂ @@ -141,22 +220,4 @@ def Program.Equiv (P₁ P₂ : Program) : Prop := notation "⟨" P₁ "⟩ " " ≋ " "⟨" P₂ "⟩" => Program.Equiv P₁ P₂ -theorem Value.Equiv.refl {P v} : Value.Equiv P v v := - match v with - | Value.const c => Value.Equiv.const - | Value.constr_app ctr_name args_rev => - let - prf : ∀ p ∈ List.zip args_rev args_rev, Value.Equiv P (Prod.fst p) (Prod.snd p) := - by sorry - Value.Equiv.constr_app prf - | Value.closure ctx body => - let - prf : ∀ v v', ⟨P⟩ v :: ctx ⊢ body ↦ v' → Expr.EvalsToEquiv P (v :: ctx) body v' := - by - intros v v' h - apply Expr.EvalsToEquiv.equiv h - apply Value.Equiv.refl - Value.Equiv.closure prf prf - | Value.unit => Value.Equiv.unit - end Juvix.Core.Main diff --git a/Juvix/Utils.lean b/Juvix/Utils.lean new file mode 100644 index 0000000..ea11308 --- /dev/null +++ b/Juvix/Utils.lean @@ -0,0 +1,40 @@ + +import Aesop + +namespace Juvix.Utils + +theorem monotone_ex_all {α} {P : Nat → α → Prop} + (mh: ∀ n n' x, P n x → n ≤ n' → P n' x) + (l : List α) + (h : ∀ x ∈ l, ∃ n, P n x) : ∃ n, ∀ x ∈ l, P n x := by + induction l with + | nil => + exists 0 + aesop + | cons x xs ih => + obtain ⟨n, hn⟩ := h x (by simp) + obtain ⟨m, hm⟩ := ih (λ x hx => h x (by simp [hx])) + exists (Max.max n m) + intros x' hx' + cases hx' + case intro.head => + apply mh + exact hn + exact Nat.le_max_left n m + case intro.tail ht => + apply (mh m (Max.max n m) x') + aesop + exact Nat.le_max_right n m + +theorem zip_refl_eq {α} (l : List α) (p : α × α) (h : p ∈ List.zip l l) : p.fst = p.snd := by + induction l with + | nil => + cases h + | cons x xs ih => + cases h + case cons.head => + simp + case cons.tail ht => + exact ih ht + +end Juvix.Utils