From a5276581ec50eeb398ede5a3c10b304fd6153bc1 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 13 Jan 2025 11:08:18 +0100 Subject: [PATCH 1/6] Value.Equiv (wip, wrong) --- Juvix/Core/Main/Language/Base.lean | 2 + Juvix/Core/Main/Semantics.lean | 83 ++++++++++++++++++++---------- 2 files changed, 57 insertions(+), 28 deletions(-) diff --git a/Juvix/Core/Main/Language/Base.lean b/Juvix/Core/Main/Language/Base.lean index 5c371ac..e7c2484 100644 --- a/Juvix/Core/Main/Language/Base.lean +++ b/Juvix/Core/Main/Language/Base.lean @@ -38,6 +38,8 @@ structure Program where defs : AssocList Name Expr main : Expr +infixr:80 "@@" => Expr.app + def Expr.mk_app (f : Expr) : List Expr → Expr | [] => f | x :: xs => Expr.mk_app (Expr.app f x) xs diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean index 71c9c1b..cb22bdd 100644 --- a/Juvix/Core/Main/Semantics.lean +++ b/Juvix/Core/Main/Semantics.lean @@ -53,10 +53,10 @@ inductive Eval (P : Program) : Context → Expr → Value → Prop where | eval_unit {ctx} : Eval P ctx Expr.unit Value.unit -notation "[" P "] " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v +notation "⟨" P "⟩ " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v -- The evaluation relation is deterministic. -theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : [P] ctx ⊢ e ↦ v₁) (h₂ : [P] ctx ⊢ e ↦ v₂) : v₁ = v₂ := by +theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : ⟨P⟩ ctx ⊢ e ↦ v₁) (h₂ : ⟨P⟩ ctx ⊢ e ↦ v₂) : v₁ = v₂ := by induction h₁ generalizing v₂ with | eval_var => cases h₂ <;> cc @@ -105,31 +105,58 @@ theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : [P] ctx ⊢ e ↦ v₁) ( | eval_unit => cases h₂ <;> cc --- The termination predicate for values. It is too strong for higher-order --- functions -- requires termination for all function arguments, even --- non-terminating ones. -inductive Value.Terminating (P : Program) : Value → Prop where - | const {c} : Value.Terminating P (Value.const c) - | constr_app {ctr_name args_rev} : - Value.Terminating P (Value.constr_app ctr_name args_rev) - | closure {ctx body} : - (∀ v v', - [P] v :: ctx ⊢ body ↦ v' → - Value.Terminating P v') → - Value.Terminating P (Value.closure ctx body) - | unit : Value.Terminating P Value.unit - -def Expr.Terminating (P : Program) (ctx : Context) (e : Expr) : Prop := - (∃ v, [P] ctx ⊢ e ↦ v ∧ Value.Terminating P v) - -def Program.Terminating (P : Program) : Prop := - Expr.Terminating P [] P.main - -lemma Eval.Expr.Terminating {P ctx e v} : - Expr.Terminating P ctx e → [P] ctx ⊢ e ↦ v → Value.Terminating P v := by - intro h₁ h₂ - rcases h₁ with ⟨v', hval, hterm⟩ - rewrite [Eval.deterministic h₂ hval] - assumption +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 +end + +notation "⟨" P "⟩ " e " ≈ " e':40 => Value.Equiv P e e' + +notation "⟨" P "⟩ " ctx " ⊢ " e " ↦≈ " v:40 => Expr.EvalsToEquiv 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) + +notation "⟨" P₁ "⟩ " ctx₁ " ⊢ " e₁ " ≋ " "⟨" P₂ "⟩ " ctx₂ " ⊢ " e₂:40 => Expr.Equiv P₁ ctx₁ e₁ P₂ ctx₂ e₂ + +def Program.Equiv (P₁ P₂ : Program) : Prop := + ⟨P₁⟩ [] ⊢ P₁.main ≋ ⟨P₂⟩ [] ⊢ P₂.main + +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 From 5249b548b91b6092dca2e849290e21a24449ed6f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 13 Jan 2025 18:40:45 +0100 Subject: [PATCH 2/6] 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 From 64d238febcc9ec1c3a0fc630ebb0d1b88eb25477 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 14 Jan 2025 14:49:43 +0100 Subject: [PATCH 3/6] approx transitivity --- Juvix/Core/Main/Semantics.lean | 85 +++++++++++++++++++++++++++++----- Juvix/Utils.lean | 31 +++++++++++++ 2 files changed, 104 insertions(+), 12 deletions(-) diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean index 36f0e6a..04cfeb3 100644 --- a/Juvix/Core/Main/Semantics.lean +++ b/Juvix/Core/Main/Semantics.lean @@ -112,6 +112,7 @@ mutual 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'} : + args_rev.length = args_rev'.length → (∀ 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₂} : @@ -122,7 +123,7 @@ mutual -- 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₂} : + | 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₁ @@ -155,12 +156,51 @@ lemma Value.Approx.Indexed.monotone {P n n' v v'} (h : Value.Approx.Indexed P n have eh : Expr.ApproxEvals.Indexed P n' (v :: ctx₂) body₂ v' := by apply ch exact h'' - rcases eh with ⟨h1, h2⟩ + rcases eh with ⟨_, h1, _⟩ constructor exact h1 aesop aesop +lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} (h₁ : Value.Approx.Indexed P n v₁ v₂) (h₂ : Value.Approx.Indexed P n v₂ v₃) : Value.Approx.Indexed P n v₁ v₃ := by + induction n generalizing v₁ v₂ v₃ with + | zero => + cases h₁ + cases h₂ + exact Value.Approx.Indexed.refl + | succ n ih => + cases h₁ + case refl => + exact h₂ + case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ => + cases h₂ + case refl => + exact Value.Approx.Indexed.constr_app hlen₁ ch₁ + case constr_app args_rev'' hlen₂ ch₂ => + constructor + · aesop + · intro p hp + obtain ⟨p₁, hp₁, p₂, hp₂, h₁, h₂, h₃⟩ := Utils.zip_ex_mid3 args_rev args_rev' args_rev'' p hlen₁ hlen₂ hp + aesop + case closure ctx₁ body₁ ctx₂ body₂ ch₁ => + cases h₂ + case refl => + exact Value.Approx.Indexed.closure ch₁ + case closure ctx₃ body₃ ch₂ => + constructor + · intro v v₁ h + have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by + apply ch₁ + exact h + rcases eh with ⟨v₂, h₁, h₂⟩ + have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₃) body₃ v₂ := by + apply ch₂ + exact h₁ + rcases eh with ⟨v₃, h₃, h₄⟩ + constructor + · exact h₃ + · aesop + def Value.Approx (P : Program) (v v' : Value) : Prop := ∃ n, Value.Approx.Indexed P n v v' @@ -175,6 +215,21 @@ lemma Value.Approx.refl {P v} : ⟨P⟩ v ≲ v := by exists 0 exact Value.Approx.Indexed.refl +lemma Value.Approx.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ v₂ ≲ v₃ → ⟨P⟩ v₁ ≲ v₃ := by + intros h₁ h₂ + obtain ⟨n₁, h₁⟩ := h₁ + obtain ⟨n₂, h₂⟩ := h₂ + exists (n₁ + n₂) + have h₁ : Indexed P (n₁ + n₂) v₁ v₂ := by + apply Value.Approx.Indexed.monotone + · exact h₁ + · aesop + have h₂ : Indexed P (n₁ + n₂) v₂ v₃ := by + apply Value.Approx.Indexed.monotone + · exact h₂ + · aesop + aesop (add unsafe apply Value.Approx.Indexed.trans) + 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] @@ -182,20 +237,27 @@ lemma Value.Approx.zip_refl {P p} {l : List Value} (h : p ∈ l.zip l) : ⟨P⟩ 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 + (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p) ∧ + args_rev.length = args_rev'.length := by + intro h rcases h with ⟨n, h⟩ - cases h - case constr_app => - constructor + constructor + case left => + intros p hp + cases h + case constr_app => + constructor + aesop + case refl => + exact Value.Approx.zip_refl hp + case right => aesop - case refl => - exact Value.Approx.zip_refl hp lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : + args_rev.length = args_rev'.length → (∀ 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 + intro hlen 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 @@ -204,8 +266,7 @@ lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : assumption obtain ⟨n, h''⟩ := nh exists (Nat.succ n) - constructor - assumption + 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) diff --git a/Juvix/Utils.lean b/Juvix/Utils.lean index ea11308..b0f8d39 100644 --- a/Juvix/Utils.lean +++ b/Juvix/Utils.lean @@ -37,4 +37,35 @@ theorem zip_refl_eq {α} (l : List α) (p : α × α) (h : p ∈ List.zip l l) : case cons.tail ht => exact ih ht +theorem zip_ex_mid3 {α} (l₁ l₂ l₃ : List α) (p : α × α) + (hl₁ : l₁.length = l₂.length) + (hl₂ : l₂.length = l₃.length) + (hp : p ∈ List.zip l₁ l₃) : + ∃ p₁ ∈ List.zip l₁ l₂, + ∃ p₂ ∈ List.zip l₂ l₃, + p.fst = p₁.fst ∧ p.snd = p₂.snd ∧ p₁.snd = p₂.fst := by + induction l₁ generalizing l₂ l₃ with + | nil => + cases hp + | cons x xs ih => + cases l₂ with + | nil => + cases l₃ + case nil => + cases hp + case cons y ys => + contradiction + | cons y ys => + cases l₃ with + | nil => + cases hp + | cons z zs => + cases hp + case cons.head => + simp + case cons.tail ht => + simp at hl₁ hl₂ + obtain ⟨p₁, hp₁, p₂, hp₂, h₁, h₂⟩ := ih ys zs hl₁ hl₂ ht + exact ⟨p₁, List.mem_cons_of_mem _ hp₁, p₂, List.mem_cons_of_mem _ hp₂, h₁, h₂⟩ + end Juvix.Utils From d2dd235f663e46aae65b0963502ba4cc18117bad Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 14 Jan 2025 17:07:37 +0100 Subject: [PATCH 4/6] refactor (wip, wrong) --- Juvix/Core/Main/Semantics.lean | 285 +-------------------------- Juvix/Core/Main/Semantics/Equiv.lean | 219 ++++++++++++++++++++ Juvix/Core/Main/Semantics/Eval.lean | 108 ++++++++++ 3 files changed, 329 insertions(+), 283 deletions(-) create mode 100644 Juvix/Core/Main/Semantics/Equiv.lean create mode 100644 Juvix/Core/Main/Semantics/Eval.lean diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean index 04cfeb3..9fa56dc 100644 --- a/Juvix/Core/Main/Semantics.lean +++ b/Juvix/Core/Main/Semantics.lean @@ -1,284 +1,3 @@ -import Juvix.Core.Main.Language -import Mathlib.Tactic.CC -import Juvix.Utils -import Aesop - -namespace Juvix.Core.Main - -def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int := - match op with - | BinaryOp.add_int => i₁ + i₂ - | BinaryOp.sub_int => i₁ - i₂ - | BinaryOp.mul_int => i₁ * i₂ - | BinaryOp.div_int => i₁ / i₂ - -inductive Eval (P : Program) : Context → Expr → Value → Prop where - | eval_var {ctx idx val} : - ctx.get? idx = some val → - Eval P ctx (Expr.var idx) val - | eval_ident {ctx name expr val} : - P.defs.find? name = some expr → - Eval P [] expr val → - Eval P ctx (Expr.ident name) val - | eval_const {ctx c} : - Eval P ctx (Expr.const c) (Value.const c) - | eval_app {ctx ctx' f body arg val val'} : - Eval P ctx f (Value.closure ctx' body) → - Eval P ctx arg val → - Eval P (val :: ctx') body val' → - Eval P ctx (Expr.app f arg) val' - | eval_constr_app {ctx ctr ctr_name ctr_args_rev arg val} : - Eval P ctx ctr (Value.constr_app ctr_name ctr_args_rev) → - Eval P ctx arg val → - Eval P ctx (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev)) - | eval_binop {ctx op arg₁ arg₂ val₁ val₂} : - Eval P ctx arg₁ (Value.const (Constant.int val₁)) → - Eval P ctx arg₂ (Value.const (Constant.int val₂)) → - Eval P ctx (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂))) - | eval_lambda {ctx body} : - Eval P ctx (Expr.lambda body) (Value.closure ctx body) - | eval_save {ctx value body val val'} : - Eval P ctx value val → - Eval P (val :: ctx) body val' → - Eval P ctx (Expr.save value body) val' - | eval_branch_matches {ctx name args_rev body val} : - Eval P (args_rev ++ ctx) body val → - Eval P (Value.constr_app name args_rev :: ctx) (Expr.branch name body _) val - | eval_branch_fails {ctx name name' next val} : - name ≠ name' → - Eval P ctx next val → - Eval P (Value.constr_app name _ :: ctx) (Expr.branch name' _ next) val - | eval_default {ctx body val} : - Eval P ctx body val → - Eval P (_ :: ctx) (Expr.default body) val - | eval_unit {ctx} : - Eval P ctx Expr.unit Value.unit - -notation "⟨" P "⟩ " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v - --- The evaluation relation is deterministic. -theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : ⟨P⟩ ctx ⊢ e ↦ v₁) (h₂ : ⟨P⟩ ctx ⊢ e ↦ v₂) : v₁ = v₂ := by - induction h₁ generalizing v₂ with - | eval_var => - cases h₂ <;> cc - | eval_ident _ _ ih => - specialize (@ih v₂) - cases h₂ <;> cc - | eval_const => - cases h₂ <;> cc - | eval_app _ _ _ ih ih' aih => - cases h₂ with - | eval_app hval harg => - apply aih - specialize (ih hval) - specialize (ih' harg) - simp_all - | eval_constr_app _ _ ih ih' => - cases h₂ with - | eval_constr_app hctr harg => - specialize (ih hctr) - specialize (ih' harg) - simp_all - | eval_binop _ _ ih₁ ih₂ => - cases h₂ with - | eval_binop h₁ h₂ => - specialize (ih₁ h₁) - specialize (ih₂ h₂) - simp_all - | eval_lambda => - cases h₂ <;> cc - | eval_save _ _ ih ih' => - cases h₂ with - | eval_save hval hbody => - specialize (ih hval) - rw [<- ih] at hbody - specialize (ih' hbody) - simp_all - | eval_branch_matches _ ih => - specialize (@ih v₂) - cases h₂ <;> cc - | eval_branch_fails _ _ ih => - specialize (@ih v₂) - cases h₂ <;> cc - | eval_default _ ih => - specialize (@ih v₂) - cases h₂ <;> cc - | eval_unit => - cases h₂ <;> cc - -mutual - @[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'} : - args_rev.length = args_rev'.length → - (∀ 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 - -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, _⟩ - constructor - exact h1 - aesop - aesop - -lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} (h₁ : Value.Approx.Indexed P n v₁ v₂) (h₂ : Value.Approx.Indexed P n v₂ v₃) : Value.Approx.Indexed P n v₁ v₃ := by - induction n generalizing v₁ v₂ v₃ with - | zero => - cases h₁ - cases h₂ - exact Value.Approx.Indexed.refl - | succ n ih => - cases h₁ - case refl => - exact h₂ - case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ => - cases h₂ - case refl => - exact Value.Approx.Indexed.constr_app hlen₁ ch₁ - case constr_app args_rev'' hlen₂ ch₂ => - constructor - · aesop - · intro p hp - obtain ⟨p₁, hp₁, p₂, hp₂, h₁, h₂, h₃⟩ := Utils.zip_ex_mid3 args_rev args_rev' args_rev'' p hlen₁ hlen₂ hp - aesop - case closure ctx₁ body₁ ctx₂ body₂ ch₁ => - cases h₂ - case refl => - exact Value.Approx.Indexed.closure ch₁ - case closure ctx₃ body₃ ch₂ => - constructor - · intro v v₁ h - have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by - apply ch₁ - exact h - rcases eh with ⟨v₂, h₁, h₂⟩ - have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₃) body₃ v₂ := by - apply ch₂ - exact h₁ - rcases eh with ⟨v₃, h₃, h₄⟩ - constructor - · exact h₃ - · 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.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ v₂ ≲ v₃ → ⟨P⟩ v₁ ≲ v₃ := by - intros h₁ h₂ - obtain ⟨n₁, h₁⟩ := h₁ - obtain ⟨n₂, h₂⟩ := h₂ - exists (n₁ + n₂) - have h₁ : Indexed P (n₁ + n₂) v₁ v₂ := by - apply Value.Approx.Indexed.monotone - · exact h₁ - · aesop - have h₂ : Indexed P (n₁ + n₂) v₂ v₃ := by - apply Value.Approx.Indexed.monotone - · exact h₂ - · aesop - aesop (add unsafe apply Value.Approx.Indexed.trans) - -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) ∧ - args_rev.length = args_rev'.length := by - intro h - rcases h with ⟨n, h⟩ - constructor - case left => - intros p hp - cases h - case constr_app => - constructor - aesop - case refl => - exact Value.Approx.zip_refl hp - case right => - aesop - -lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ 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 hlen 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 := - 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₂ - -def Program.Equiv (P₁ P₂ : Program) : Prop := - ⟨P₁⟩ [] ⊢ P₁.main ≋ ⟨P₂⟩ [] ⊢ P₂.main - -notation "⟨" P₁ "⟩ " " ≋ " "⟨" P₂ "⟩" => Program.Equiv P₁ P₂ - -end Juvix.Core.Main +import Juvix.Core.Main.Semantics.Eval +import Juvix.Core.Main.Semantics.Equiv diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean new file mode 100644 index 0000000..184d4d1 --- /dev/null +++ b/Juvix/Core/Main/Semantics/Equiv.lean @@ -0,0 +1,219 @@ + +import Juvix.Core.Main.Semantics.Eval +import Juvix.Utils +import Aesop + +namespace Juvix.Core.Main + +mutual + @[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'} : + args_rev.length = args_rev'.length → + (∀ 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 + +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 + +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 := + 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₂ + +def Program.Equiv (P₁ P₂ : Program) : Prop := + ⟨P₁⟩ [] ⊢ P₁.main ≋ ⟨P₂⟩ [] ⊢ P₂.main + +notation "⟨" P₁ "⟩ " " ≋ " "⟨" P₂ "⟩" => Program.Equiv P₁ P₂ + +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, _⟩ + constructor + exact h1 + aesop + aesop + +lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} (h₁ : Value.Approx.Indexed P n v₁ v₂) (h₂ : Value.Approx.Indexed P n v₂ v₃) : Value.Approx.Indexed P n v₁ v₃ := by + induction n generalizing v₁ v₂ v₃ with + | zero => + cases h₁ + cases h₂ + exact Value.Approx.Indexed.refl + | succ n ih => + cases h₁ + case refl => + exact h₂ + case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ => + cases h₂ + case refl => + exact Value.Approx.Indexed.constr_app hlen₁ ch₁ + case constr_app args_rev'' hlen₂ ch₂ => + constructor + · aesop + · intro p hp + obtain ⟨p₁, hp₁, p₂, hp₂, h₁, h₂, h₃⟩ := Utils.zip_ex_mid3 args_rev args_rev' args_rev'' p hlen₁ hlen₂ hp + aesop + case closure ctx₁ body₁ ctx₂ body₂ ch₁ => + cases h₂ + case refl => + exact Value.Approx.Indexed.closure ch₁ + case closure ctx₃ body₃ ch₂ => + constructor + · intro v v₁ h + have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by + apply ch₁ + exact h + rcases eh with ⟨v₂, h₁, h₂⟩ + have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₃) body₃ v₂ := by + apply ch₂ + exact h₁ + rcases eh with ⟨v₃, h₃, h₄⟩ + constructor + · exact h₃ + · aesop + +lemma Value.Approx.refl {P v} : ⟨P⟩ v ≲ v := by + exists 0 + exact Value.Approx.Indexed.refl + +lemma Value.Approx.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ v₂ ≲ v₃ → ⟨P⟩ v₁ ≲ v₃ := by + intros h₁ h₂ + obtain ⟨n₁, h₁⟩ := h₁ + obtain ⟨n₂, h₂⟩ := h₂ + exists (n₁ + n₂) + have h₁ : Indexed P (n₁ + n₂) v₁ v₂ := by + apply Value.Approx.Indexed.monotone + · exact h₁ + · aesop + have h₂ : Indexed P (n₁ + n₂) v₂ v₃ := by + apply Value.Approx.Indexed.monotone + · exact h₂ + · aesop + aesop (add unsafe apply Value.Approx.Indexed.trans) + +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) ∧ + args_rev.length = args_rev'.length := by + intro h + rcases h with ⟨n, h⟩ + constructor + case left => + intros p hp + cases h + case constr_app => + constructor + aesop + case refl => + exact Value.Approx.zip_refl hp + case right => + aesop + +lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : + args_rev.length = args_rev'.length → + (∀ 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 hlen 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 + +lemma Value.Approx.closure_inv {P ctx₁ body₁ ctx₂ body₂} : + ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ → + ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁ := by + intro h + rcases h with ⟨n, h⟩ + cases h + case refl => + intro v v₁ h + exists 0 + constructor + exact h + exact Value.Approx.Indexed.refl + case closure n h => + intro v v₁ h' + have h' : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by + apply h + exact h' + rcases h' with ⟨v₂, h₁, h₂⟩ + constructor + aesop + +lemma Value.Approx.closure {P ctx₁ body₁ ctx₂ body₂} : + (∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁) → + ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ := by + intro h + have h' : ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ∃ n, Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by + intros v v₁ h' + have h' : ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁ := by + apply h + exact h' + rcases h' with ⟨n, v₂, h₂⟩ + constructor + constructor + exact h₂ + assumption + sorry + +end Juvix.Core.Main diff --git a/Juvix/Core/Main/Semantics/Eval.lean b/Juvix/Core/Main/Semantics/Eval.lean new file mode 100644 index 0000000..6dd4b6d --- /dev/null +++ b/Juvix/Core/Main/Semantics/Eval.lean @@ -0,0 +1,108 @@ + +import Juvix.Core.Main.Language +import Mathlib.Tactic.CC + +namespace Juvix.Core.Main + +def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int := + match op with + | BinaryOp.add_int => i₁ + i₂ + | BinaryOp.sub_int => i₁ - i₂ + | BinaryOp.mul_int => i₁ * i₂ + | BinaryOp.div_int => i₁ / i₂ + +inductive Eval (P : Program) : Context → Expr → Value → Prop where + | eval_var {ctx idx val} : + ctx.get? idx = some val → + Eval P ctx (Expr.var idx) val + | eval_ident {ctx name expr val} : + P.defs.find? name = some expr → + Eval P [] expr val → + Eval P ctx (Expr.ident name) val + | eval_const {ctx c} : + Eval P ctx (Expr.const c) (Value.const c) + | eval_app {ctx ctx' f body arg val val'} : + Eval P ctx f (Value.closure ctx' body) → + Eval P ctx arg val → + Eval P (val :: ctx') body val' → + Eval P ctx (Expr.app f arg) val' + | eval_constr_app {ctx ctr ctr_name ctr_args_rev arg val} : + Eval P ctx ctr (Value.constr_app ctr_name ctr_args_rev) → + Eval P ctx arg val → + Eval P ctx (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev)) + | eval_binop {ctx op arg₁ arg₂ val₁ val₂} : + Eval P ctx arg₁ (Value.const (Constant.int val₁)) → + Eval P ctx arg₂ (Value.const (Constant.int val₂)) → + Eval P ctx (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂))) + | eval_lambda {ctx body} : + Eval P ctx (Expr.lambda body) (Value.closure ctx body) + | eval_save {ctx value body val val'} : + Eval P ctx value val → + Eval P (val :: ctx) body val' → + Eval P ctx (Expr.save value body) val' + | eval_branch_matches {ctx name args_rev body val} : + Eval P (args_rev ++ ctx) body val → + Eval P (Value.constr_app name args_rev :: ctx) (Expr.branch name body _) val + | eval_branch_fails {ctx name name' next val} : + name ≠ name' → + Eval P ctx next val → + Eval P (Value.constr_app name _ :: ctx) (Expr.branch name' _ next) val + | eval_default {ctx body val} : + Eval P ctx body val → + Eval P (_ :: ctx) (Expr.default body) val + | eval_unit {ctx} : + Eval P ctx Expr.unit Value.unit + +notation "⟨" P "⟩ " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v + +-- The evaluation relation is deterministic. +theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : ⟨P⟩ ctx ⊢ e ↦ v₁) (h₂ : ⟨P⟩ ctx ⊢ e ↦ v₂) : v₁ = v₂ := by + induction h₁ generalizing v₂ with + | eval_var => + cases h₂ <;> cc + | eval_ident _ _ ih => + specialize (@ih v₂) + cases h₂ <;> cc + | eval_const => + cases h₂ <;> cc + | eval_app _ _ _ ih ih' aih => + cases h₂ with + | eval_app hval harg => + apply aih + specialize (ih hval) + specialize (ih' harg) + simp_all + | eval_constr_app _ _ ih ih' => + cases h₂ with + | eval_constr_app hctr harg => + specialize (ih hctr) + specialize (ih' harg) + simp_all + | eval_binop _ _ ih₁ ih₂ => + cases h₂ with + | eval_binop h₁ h₂ => + specialize (ih₁ h₁) + specialize (ih₂ h₂) + simp_all + | eval_lambda => + cases h₂ <;> cc + | eval_save _ _ ih ih' => + cases h₂ with + | eval_save hval hbody => + specialize (ih hval) + rw [<- ih] at hbody + specialize (ih' hbody) + simp_all + | eval_branch_matches _ ih => + specialize (@ih v₂) + cases h₂ <;> cc + | eval_branch_fails _ _ ih => + specialize (@ih v₂) + cases h₂ <;> cc + | eval_default _ ih => + specialize (@ih v₂) + cases h₂ <;> cc + | eval_unit => + cases h₂ <;> cc + +end Juvix.Core.Main From 120774ba6e9360a514e02af468b373068ac346e1 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 14 Jan 2025 18:54:52 +0100 Subject: [PATCH 5/6] Value.Approx correction --- Juvix/Core/Main/Semantics/Equiv.lean | 229 +++++++++++++-------------- Juvix/Core/Main/Semantics/Eval.lean | 5 + 2 files changed, 119 insertions(+), 115 deletions(-) diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean index 184d4d1..421b167 100644 --- a/Juvix/Core/Main/Semantics/Equiv.lean +++ b/Juvix/Core/Main/Semantics/Equiv.lean @@ -1,6 +1,7 @@ import Juvix.Core.Main.Semantics.Eval import Juvix.Utils +import Mathlib.Tactic.Linarith import Aesop namespace Juvix.Core.Main @@ -8,14 +9,15 @@ namespace Juvix.Core.Main mutual @[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 + | unit {n} : Value.Approx.Indexed P n Value.unit Value.unit + | const {n c} : Value.Approx.Indexed P n (Value.const c) (Value.const c) | constr_app {n ctr_name args_rev args_rev'} : args_rev.length = args_rev'.length → - (∀ 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') + (∀ k < n, ∀ p ∈ List.zip args_rev args_rev', Value.Approx.Indexed P k (Prod.fst p) (Prod.snd p)) → + Value.Approx.Indexed P 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₂) + (∀ k < n, ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → Expr.ApproxEvals.Indexed P k (v :: ctx₂) body₂ v₁) → + Value.Approx.Indexed P 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`. @@ -28,10 +30,10 @@ mutual end def Value.Approx (P : Program) (v v' : Value) : Prop := - ∃ n, Value.Approx.Indexed P n v v' + ∀ 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 + ∀ n, Expr.ApproxEvals.Indexed P n ctx e v notation "⟨" P "⟩ " e " ≲ " e':40 => Value.Approx P e e' @@ -50,95 +52,125 @@ def Program.Equiv (P₁ P₂ : Program) : Prop := notation "⟨" P₁ "⟩ " " ≋ " "⟨" P₂ "⟩" => Program.Equiv P₁ P₂ -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 +lemma Value.Approx.Indexed.refl {P n v} : Value.Approx.Indexed P n v v := by + revert n + suffices ∀ n, ∀ k ≤ n, Value.Approx.Indexed P k v v by + intro k + exact this k k k.le_refl + intro n + induction n generalizing 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 => + intros k hk + cases v + case unit => + exact Value.Approx.Indexed.unit + case const c => + exact Value.Approx.Indexed.const + case constr_app ctr_name args_rev => + constructor + · rfl + · intros + have : k = 0 := by linarith + subst k + contradiction + case closure ctx body => + constructor + · intros + have : k = 0 := by linarith + subst k + contradiction + | succ n ih => + intros k hk + cases v + case unit => + exact Value.Approx.Indexed.unit + case const c => + exact Value.Approx.Indexed.const + case constr_app ctr_name args_rev => + constructor + · rfl + · intros k' hk' p hp + have h : p.fst = p.snd := Utils.zip_refl_eq args_rev p hp + rw [h] + have : k' ≤ n := by linarith 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, _⟩ - constructor - exact h1 - aesop + case closure ctx body => + constructor + · intros k' hk' v v' + have : k' ≤ n := by linarith aesop -lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} (h₁ : Value.Approx.Indexed P n v₁ v₂) (h₂ : Value.Approx.Indexed P n v₂ v₃) : Value.Approx.Indexed P n v₁ v₃ := by +lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} : Value.Approx.Indexed P n v₁ v₂ → Value.Approx.Indexed P n v₂ v₃ → Value.Approx.Indexed P n v₁ v₃ := by + revert n + suffices ∀ n, ∀ k ≤ n, Indexed P k v₁ v₂ → Indexed P k v₂ v₃ → Value.Approx.Indexed P k v₁ v₃ by + intro k + exact this k k k.le_refl + intros n induction n generalizing v₁ v₂ v₃ with | zero => + intros k hk h₁ h₂ cases h₁ - cases h₂ - exact Value.Approx.Indexed.refl + case unit => + cases h₂ + case unit => + exact Value.Approx.Indexed.unit + case const => + cases h₂ + case const => + exact Value.Approx.Indexed.const + case constr_app ctr_name args_rev₁ args_rev₁' hlen₁ ch₁ => + cases h₂ + case constr_app args_rev₂ hlen₂ ch₂ => + constructor <;> aesop + case closure ctx₁ body₁ ctx₁' body₁' ch₁ => + cases h₂ + case closure ctx₂ body₂ ch₂ => + constructor + · intro k' hk' v v₁ h + have : k = 0 := by linarith + subst k + contradiction | succ n ih => + intros k hk h₁ h₂ cases h₁ - case refl => - exact h₂ + case unit => + cases h₂ + case unit => + exact Value.Approx.Indexed.unit + case const => + cases h₂ + case const => + exact Value.Approx.Indexed.const case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ => cases h₂ - case refl => - exact Value.Approx.Indexed.constr_app hlen₁ ch₁ case constr_app args_rev'' hlen₂ ch₂ => constructor · aesop - · intro p hp + · intro k' hk' p hp obtain ⟨p₁, hp₁, p₂, hp₂, h₁, h₂, h₃⟩ := Utils.zip_ex_mid3 args_rev args_rev' args_rev'' p hlen₁ hlen₂ hp + have : k' ≤ n := by linarith aesop case closure ctx₁ body₁ ctx₂ body₂ ch₁ => cases h₂ - case refl => - exact Value.Approx.Indexed.closure ch₁ case closure ctx₃ body₃ ch₂ => constructor - · intro v v₁ h - have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by - apply ch₁ - exact h - rcases eh with ⟨v₂, h₁, h₂⟩ - have eh : Expr.ApproxEvals.Indexed P n (v :: ctx₃) body₃ v₂ := by - apply ch₂ - exact h₁ - rcases eh with ⟨v₃, h₃, h₄⟩ - constructor - · exact h₃ - · aesop + · intro k' hk' v v₁ h + have ah₁ : Expr.ApproxEvals.Indexed P k' (v :: ctx₂) body₂ v₁ := by + apply ch₁ <;> assumption + obtain ⟨v₂, _, h₂⟩ := ah₁ + have ah₂ : Expr.ApproxEvals.Indexed P k' (v :: ctx₃) body₃ v₂ := by + apply ch₂ <;> assumption + obtain ⟨v₃, _, h₃⟩ := ah₂ + have : k' ≤ n := by linarith + aesop lemma Value.Approx.refl {P v} : ⟨P⟩ v ≲ v := by - exists 0 + intro n exact Value.Approx.Indexed.refl lemma Value.Approx.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ v₂ ≲ v₃ → ⟨P⟩ v₁ ≲ v₃ := by intros h₁ h₂ - obtain ⟨n₁, h₁⟩ := h₁ - obtain ⟨n₂, h₂⟩ := h₂ - exists (n₁ + n₂) - have h₁ : Indexed P (n₁ + n₂) v₁ v₂ := by - apply Value.Approx.Indexed.monotone - · exact h₁ - · aesop - have h₂ : Indexed P (n₁ + n₂) v₂ v₃ := by - apply Value.Approx.Indexed.monotone - · exact h₂ - · aesop + intro n aesop (add unsafe apply Value.Approx.Indexed.trans) lemma Value.Approx.zip_refl {P p} {l : List Value} (h : p ∈ l.zip l) : ⟨P⟩ p.fst ≲ p.snd := by @@ -151,69 +183,36 @@ lemma Value.Approx.constr_app_inv {P ctr_name args_rev args_rev'} : (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p) ∧ args_rev.length = args_rev'.length := by intro h - rcases h with ⟨n, h⟩ constructor case left => - intros p hp - cases h + intros p hp n + cases (h (n + 1)) case constr_app => - constructor aesop - case refl => - exact Value.Approx.zip_refl hp case right => - aesop + cases (h 0) + case constr_app => + aesop lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : args_rev.length = args_rev'.length → (∀ 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 hlen 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 + intro hlen h n + aesop lemma Value.Approx.closure_inv {P ctx₁ body₁ ctx₂ body₂} : ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ → ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁ := by - intro h - rcases h with ⟨n, h⟩ - cases h - case refl => - intro v v₁ h - exists 0 - constructor - exact h - exact Value.Approx.Indexed.refl - case closure n h => - intro v v₁ h' - have h' : Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by - apply h - exact h' - rcases h' with ⟨v₂, h₁, h₂⟩ - constructor + intro h v v₁ h' n + cases (h n.succ) + case closure h => aesop lemma Value.Approx.closure {P ctx₁ body₁ ctx₂ body₂} : (∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁) → ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ := by - intro h - have h' : ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ∃ n, Expr.ApproxEvals.Indexed P n (v :: ctx₂) body₂ v₁ := by - intros v v₁ h' - have h' : ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁ := by - apply h - exact h' - rcases h' with ⟨n, v₂, h₂⟩ - constructor - constructor - exact h₂ - assumption - sorry + intro h n + aesop end Juvix.Core.Main diff --git a/Juvix/Core/Main/Semantics/Eval.lean b/Juvix/Core/Main/Semantics/Eval.lean index 6dd4b6d..93bfd24 100644 --- a/Juvix/Core/Main/Semantics/Eval.lean +++ b/Juvix/Core/Main/Semantics/Eval.lean @@ -55,6 +55,11 @@ inductive Eval (P : Program) : Context → Expr → Value → Prop where notation "⟨" P "⟩ " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v +def Terminating (P : Program) (ctx : Context) (e : Expr) : Prop := + ∃ v, ⟨P⟩ ctx ⊢ e ↦ v + +notation "⟨" P "⟩ " ctx " ⊢ " e:40 " ↓" => Terminating P ctx e + -- The evaluation relation is deterministic. theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : ⟨P⟩ ctx ⊢ e ↦ v₁) (h₂ : ⟨P⟩ ctx ⊢ e ↦ v₂) : v₁ = v₂ := by induction h₁ generalizing v₂ with From fb63d0c1c0666659af20a7eeae16355f1e12366f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 15 Jan 2025 10:55:01 +0100 Subject: [PATCH 6/6] minor refactor --- Juvix/Core/Main/Semantics/Equiv.lean | 29 ++++++++++++---------------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean index 421b167..8fc6d13 100644 --- a/Juvix/Core/Main/Semantics/Equiv.lean +++ b/Juvix/Core/Main/Semantics/Equiv.lean @@ -173,10 +173,18 @@ lemma Value.Approx.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ intro n aesop (add unsafe apply Value.Approx.Indexed.trans) -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 {P ctr_name args_rev args_rev'} : + args_rev.length = args_rev'.length → + (∀ 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 hlen h n + aesop + +lemma Value.Approx.closure {P ctx₁ body₁ ctx₂ body₂} : + (∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁) → + ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ := by + intro h n + aesop 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' → @@ -194,13 +202,6 @@ lemma Value.Approx.constr_app_inv {P ctr_name args_rev args_rev'} : case constr_app => aesop -lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ 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 hlen h n - aesop - lemma Value.Approx.closure_inv {P ctx₁ body₁ ctx₂ body₂} : ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ → ∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁ := by @@ -209,10 +210,4 @@ lemma Value.Approx.closure_inv {P ctx₁ body₁ ctx₂ body₂} : case closure h => aesop -lemma Value.Approx.closure {P ctx₁ body₁ ctx₂ body₂} : - (∀ v v₁, ⟨P⟩ v :: ctx₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: ctx₂ ⊢ body₂ ↦≳ v₁) → - ⟨P⟩ Value.closure ctx₁ body₁ ≲ Value.closure ctx₂ body₂ := by - intro h n - aesop - end Juvix.Core.Main