Skip to content

Commit

Permalink
args approx
Browse files Browse the repository at this point in the history
  • Loading branch information
@lukaszcz
lukaszcz committed Jan 24, 2025
1 parent ca18db5 commit 7367808
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 56 deletions.
122 changes: 66 additions & 56 deletions Juvix/Core/Main/Semantics/Equiv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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₂ ∧
Expand All @@ -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₂)

Expand All @@ -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]
Expand Down Expand Up @@ -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 →
Expand All @@ -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

Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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₂ =>
Expand All @@ -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₂ =>
Expand Down Expand Up @@ -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₂} :
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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₂) →
Expand Down
15 changes: 15 additions & 0 deletions Juvix/Utils.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@

import Mathlib.Order.Defs.Unbundled
import Aesop

namespace Juvix.Utils
Expand Down Expand Up @@ -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

0 comments on commit 7367808

Please sign in to comment.