diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean index 82eff1a..77509ac 100644 --- a/Juvix/Core/Main/Semantics/Equiv.lean +++ b/Juvix/Core/Main/Semantics/Equiv.lean @@ -3,6 +3,7 @@ import Juvix.Core.Main.Semantics.Eval import Juvix.Core.Main.Semantics.Eval.Indexed import Juvix.Utils import Mathlib.Tactic.Linarith +import Mathlib.Data.List.Forall2 import Aesop namespace Juvix.Core.Main @@ -13,9 +14,7 @@ def Value.Approx.Indexed (n : Nat) (v₁ v₂ : Value) : Prop := (∃ ctr_name args_rev args_rev', v₁ = Value.constr_app ctr_name args_rev ∧ v₂ = Value.constr_app ctr_name args_rev' ∧ - args_rev.length = args_rev'.length ∧ - (∀ k < n, ∀ p ∈ List.zip args_rev args_rev', - Value.Approx.Indexed k (Prod.fst p) (Prod.snd p))) ∨ + (∀ k < n, List.Forall₂ (Value.Approx.Indexed k) args_rev args_rev')) ∨ (∃ env₁ body₁ env₂ body₂, v₁ = Value.closure env₁ body₁ ∧ v₂ = Value.closure env₂ body₂ ∧ @@ -29,11 +28,24 @@ def Value.Approx.Indexed (n : Nat) (v₁ v₂ : Value) : Prop := notation:40 v:40 " ≲(" n:40 ") " v':40 => Value.Approx.Indexed n v v' +notation:40 args₁:40 " ≲ₐ(" n:40 ") " args₂:40 => List.Forall₂ (Value.Approx.Indexed n) args₁ args₂ + def Value.Approx (v v' : Value) : Prop := ∀ n, v ≲(n) v' notation:40 v:40 " ≲ " v':40 => Value.Approx v v' +notation:40 args₁:40 " ≲ₐ " args₂:40 => List.Forall₂ Value.Approx args₁ args₂ + +def Object.Value.Approx.Indexed (n : Nat) : Object → Object → Prop + | Object.value v₁, Object.value v₂ => v₁ ≲(n) v₂ + | _, _ => False + +def Env.Approx.Indexed (n : Nat) : (env₁ env₂ : Env) → Prop := + List.Forall₂ (Object.Value.Approx.Indexed n) + +notation:40 env₁:40 " ≲ₑ(" n:40 ") " env₂:40 => Env.Approx.Indexed n env₁ env₂ + def Expr.Approx (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop := (∀ v₁, env₁ ⊢ e₁ ↦ v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ v₂) @@ -56,10 +68,9 @@ lemma Value.Approx.Indexed.const {n c} : Value.const c ≲(n) Value.const c := b @[aesop unsafe apply] lemma Value.Approx.Indexed.constr_app {n ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ k < n, ∀ p ∈ List.zip args_rev args_rev', p.1 ≲(k) p.2) → + (∀ k < n, args_rev ≲ₐ(k) args_rev') → Value.constr_app ctr_name args_rev ≲(n) Value.constr_app ctr_name args_rev' := by - intro hlen h + intro h unfold Value.Approx.Indexed simp only [reduceCtorEq, and_self, exists_const, constr_app.injEq, Prod.forall, exists_and_left, false_and, or_false, false_or] @@ -90,8 +101,7 @@ inductive Value.Approx.Indexed.Inversion (n : Nat) : Value → Value → Prop wh | unit : Value.Approx.Indexed.Inversion n Value.unit Value.unit | const {c} : Value.Approx.Indexed.Inversion n (Value.const c) (Value.const c) | constr_app {ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ k < n, ∀ p ∈ List.zip args_rev args_rev', p.1 ≲(k) p.2) → + (∀ k < n, args_rev ≲ₐ(k) args_rev') → Value.Approx.Indexed.Inversion n (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev') | closure {env₁ body₁ env₂ body₂} : (∀ n₁ n₂, n₁ + n₂ < n → @@ -111,14 +121,14 @@ lemma Value.Approx.Indexed.invert {n v v'} : rcases h with ⟨h₁, h₂⟩ | ⟨c, h₁, h₂⟩ | - ⟨ctr_name, args_rev, args_rev', h₁, h₂, hlen, hargs⟩ | + ⟨ctr_name, args_rev, args_rev', h₁, h₂, hargs⟩ | ⟨env₁, body₁, env₂, body₂, h₁, h₂, h⟩ · subst h₁ h₂ exact Value.Approx.Indexed.Inversion.unit · subst h₁ h₂ exact Value.Approx.Indexed.Inversion.const · subst h₁ h₂ - exact Value.Approx.Indexed.Inversion.constr_app hlen hargs + exact Value.Approx.Indexed.Inversion.constr_app hargs · subst h₁ h₂ exact Value.Approx.Indexed.Inversion.closure h @@ -138,9 +148,8 @@ lemma Value.Approx.Indexed.anti_monotone {n n' v₁ v₂} (h : v₁ ≲(n) v₂) exact Value.Approx.Indexed.unit case const => exact Value.Approx.Indexed.const - case constr_app ctr_name args_rev args_rev' hlen hargs => + case constr_app ctr_name args_rev args_rev' hargs => apply Value.Approx.Indexed.constr_app - · assumption · intros have : k = 0 := by linarith subst k @@ -158,12 +167,11 @@ lemma Value.Approx.Indexed.anti_monotone {n n' v₁ v₂} (h : v₁ ≲(n) v₂) exact Value.Approx.Indexed.unit case const => exact Value.Approx.Indexed.const - case constr_app ctr_name args_rev args_rev' hlen hargs => + case constr_app ctr_name args_rev args_rev' hargs => apply Value.Approx.Indexed.constr_app - · assumption - · intros k' hk' p hp - have h : k' ≤ n := by linarith - aesop + · intros k' hk' + have : k' < n + 1 := by linarith + simp_all only case closure env₁ body₁ env₂ body₂ ch => apply Value.Approx.Indexed.closure · intro n₁ n₂ hn a₁ a₂ v₁ happrox heval @@ -189,7 +197,6 @@ lemma Value.Approx.Indexed.refl {n} v : v ≲(n) v := by exact Value.Approx.Indexed.const case constr_app ctr_name args_rev => apply Value.Approx.Indexed.constr_app - · rfl · intros have : k = 0 := by linarith subst k @@ -209,12 +216,11 @@ lemma Value.Approx.Indexed.refl {n} v : v ≲(n) v := by exact Value.Approx.Indexed.const case constr_app ctr_name args_rev => apply Value.Approx.Indexed.constr_app - · rfl - · intros k' hk' p hp - have h : p.fst = p.snd := Utils.zip_refl_eq args_rev p hp - rw [h] + · intros k' hk' have : k' ≤ n := by linarith - aesop + rw [List.forall₂_same] + intros + simp_all only case closure env body => apply Value.Approx.Indexed.closure · intros k' hk' va₁ va₂ v₁ happrox heval @@ -239,10 +245,10 @@ lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂ invert h₂ case const => exact Value.Approx.Indexed.const - case constr_app ctr_name args_rev₁ args_rev₁' hlen₁ ch₁ => + case constr_app ctr_name args_rev₁ args_rev₁' ch₁ => cases h₂.invert - case constr_app args_rev₂ hlen₂ ch₂ => - apply Value.Approx.Indexed.constr_app <;> aesop + case constr_app args_rev₂ ch₂ => + apply Value.Approx.Indexed.constr_app; aesop case closure env₁ body₁ env₁' body₁' ch₁ => cases h₂.invert case closure env₂ body₂ ch₂ => @@ -262,15 +268,18 @@ lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂ invert h₂ case const => exact Value.Approx.Indexed.const - case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ => + case constr_app ctr_name args_rev args_rev' ch₁ => invert h₂ - case constr_app args_rev'' hlen₂ ch₂ => + case constr_app args_rev'' ch₂ => apply Value.Approx.Indexed.constr_app - · aesop - · 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 + · intro k' hk' + have hk' : k' ≤ n := by linarith + apply Utils.forall₂_trans + · unfold Transitive + intro v₁ v₂ v₃ + exact ih k' hk' + · aesop + · aesop case closure env₁ body₁ env₂ body₂ ch₁ => invert h₂ case closure env₃ body₃ ch₂ => @@ -362,10 +371,12 @@ lemma Value.Approx.const_right {v c} : Value.const c ≲ v ↔ v = Value.const c @[aesop unsafe apply] lemma Value.Approx.constr_app {ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p) → + args_rev ≲ₐ args_rev' → Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' := by - intro hlen h n + intro h n + apply Value.Approx.Indexed.constr_app + intro k hk + rw [List.forall₂_iff_zip] at * aesop lemma Value.Approx.closure {env₁ body₁ env₂ body₂} : @@ -379,37 +390,38 @@ lemma Value.Approx.closure {env₁ body₁ env₂ body₂} : @[aesop safe destruct] lemma Value.Approx.constr_app_inv {ctr_name args_rev args_rev'} : Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' → - (∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p) ∧ - args_rev.length = args_rev'.length := by + args_rev ≲ₐ args_rev' := by + rw [List.forall₂_iff_zip] intro h constructor case left => - intros p hp n - invert (h (n + 1)) - aesop + invert (h 1) + case constr_app hargs => + specialize (hargs 0 _) + · linarith + · exact List.Forall₂.length_eq hargs case right => - invert (h 0) - aesop + intros v₁ v₂ hv n + invert (h (n + 1)) + case constr_app hargs => + specialize (hargs n _) + · linarith + · rw [List.forall₂_iff_zip] at hargs + aesop lemma Value.Approx.constr_app_inv_length {ctr_name args_rev args_rev'} : Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' → args_rev.length = args_rev'.length := by intro h - exact (Value.Approx.constr_app_inv h).right - -lemma Value.Approx.constr_app_inv_args {ctr_name args_rev args_rev'} : - Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' → - ∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p := by - intro h - exact (Value.Approx.constr_app_inv h).left + have := Value.Approx.constr_app_inv h + exact List.Forall₂.length_eq this @[aesop unsafe 90% destruct] lemma Value.Approx.constr_app_inv_left {ctr_name args_rev' v} : v ≲ Value.constr_app ctr_name args_rev' → ∃ args_rev, v = Value.constr_app ctr_name args_rev ∧ - args_rev.length = args_rev'.length ∧ - ∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p := by + args_rev ≲ₐ args_rev' := by intro h invert (h 0) aesop @@ -419,8 +431,7 @@ lemma Value.Approx.constr_app_inv_right {ctr_name args_rev v} : Value.constr_app ctr_name args_rev ≲ v → ∃ args_rev', v = Value.constr_app ctr_name args_rev' ∧ - args_rev.length = args_rev'.length ∧ - ∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p := by + args_rev ≲ₐ args_rev' := by intro h invert (h 0) aesop @@ -475,8 +486,7 @@ inductive Value.Approx.Inversion : Value -> Value -> Prop where | unit : Value.Approx.Inversion Value.unit Value.unit | const {c} : Value.Approx.Inversion (Value.const c) (Value.const c) | constr_app {ctr_name args_rev args_rev'} : - args_rev.length = args_rev'.length → - (∀ p ∈ List.zip args_rev args_rev', p.1 ≲ p.2) → + args_rev ≲ₐ args_rev' → Value.Approx.Inversion (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev') | closure {env₁ body₁ env₂ body₂} : (∀ a₁ a₂, a₁ ≲ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) → diff --git a/Juvix/Utils.lean b/Juvix/Utils.lean index b0f8d39..4347d9a 100644 --- a/Juvix/Utils.lean +++ b/Juvix/Utils.lean @@ -1,4 +1,5 @@ +import Mathlib.Order.Defs.Unbundled import Aesop namespace Juvix.Utils @@ -68,4 +69,18 @@ theorem zip_ex_mid3 {α} (l₁ l₂ l₃ : List α) (p : α × α) 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₂⟩ +theorem forall₂_trans {α} {P : α → α → Prop} (h : Transitive P) : Transitive (List.Forall₂ P) := by + intro l₁ l₂ l₃ h₁ h₂ + induction h₁ generalizing l₃ + case nil => + cases h₂ + case nil => + constructor + case cons x y xs ys h₁ h₂ ih => + cases h₂ + case cons y' ys' h₂' h₃ => + constructor + exact h h₁ h₂' + exact ih h₃ + end Juvix.Utils