Approx & its monotonicity

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

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

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