Program equivalence for Juvix.Core.Main

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

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,135 +1,3 @@
 
-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
-
--- 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
-
-end Juvix.Core.Main
+import Juvix.Core.Main.Semantics.Eval
+import Juvix.Core.Main.Semantics.Equiv

Juvix/Core/Main/Semantics/Equiv.lean

@@ -0,0 +1,218 @@
+
+import Juvix.Core.Main.Semantics.Eval
+import Juvix.Utils
+import Mathlib.Tactic.Linarith
+import Aesop
+
+namespace Juvix.Core.Main
+
+mutual
+  @[aesop unsafe [constructors, cases]]
+  inductive Value.Approx.Indexed (P : Program) : Nat → Value → Value → Prop where
+    | 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 →
+      (∀ 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₂} :
+      (∀ 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`.
+  @[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.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 =>
+    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 ctx body =>
+      constructor
+      · intros k' hk' v v'
+        have : k' ≤ n := by linarith
+        aesop
+
+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₁
+    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 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
+        · 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 closure ctx₃ body₃ ch₂ =>
+        constructor
+        · 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
+  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₂
+  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_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
+  constructor
+  case left =>
+    intros p hp n
+    cases (h (n + 1))
+    case constr_app =>
+      aesop
+  case right =>
+    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 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 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 n
+  aesop
+
+end Juvix.Core.Main