'invert' tactic

anoma · Jan 24, 2025 · 8164b76 · 8164b76
1 parent 6aee2d7
commit 8164b76
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 29 deletions.
diff --git a/Juvix/Core/Main/Evaluator.lean b/Juvix/Core/Main/Evaluator.lean
@@ -24,7 +24,7 @@ partial def eval (env : Env) : Expr -> Value
   | Expr.lambda body => Value.closure env body
   | Expr.save value body => eval (eval env value ∷ env) body
   | Expr.branch name body next => match env with
-    | Value.constr_app name' args_rev ∷ env' =>
+    | Object.value (Value.constr_app name' args_rev) :: env' =>
       if name = name' then
         eval (args_rev.map Object.value ++ env') body
       else

diff --git a/Juvix/Core/Main/Language/Value.lean b/Juvix/Core/Main/Language/Value.lean
@@ -18,7 +18,8 @@ mutual
 end
 
 abbrev Env : Type := List Object
+abbrev cons_value (v : Value) (env : Env) : Env := Object.value v :: env
 
-infixr:50 " ∷ " => fun x y => Object.value x :: y
+infixr:50 " ∷ " => cons_value
 
 end Juvix.Core.Main
diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean
@@ -122,6 +122,8 @@ lemma Value.Approx.Indexed.invert {n v v'} :
   · subst h₁ h₂
     exact Value.Approx.Indexed.Inversion.closure h
 
+macro "invert" h:term : tactic => `(tactic| (cases ($h).invert; try clear $h))
+
 @[refl]
 lemma Value.Approx.Indexed.refl {n} v : v ≲(n) v := by
   revert n
@@ -171,7 +173,6 @@ lemma Value.Approx.Indexed.refl {n} v : v ≲(n) v := by
         have : k' ≤ n := by linarith
         sorry
 
-@[trans]
 lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂ ≲(n) v₃ → v₁ ≲(n) v₃ := by
   revert n
   suffices ∀ n, ∀ k ≤ n, v₁ ≲(k) v₂ → v₂ ≲(k) v₃ → v₁ ≲(k) v₃ by
@@ -181,13 +182,13 @@ lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂
   induction n generalizing v₁ v₂ v₃ with
   | zero =>
     intros k hk h₁ h₂
-    cases h₁.invert
+    invert h₁
     case unit =>
-      cases h₂.invert
+      invert h₂
       case unit =>
         exact Value.Approx.Indexed.unit
     case const =>
-      cases h₂.invert
+      invert h₂
       case const =>
         exact Value.Approx.Indexed.const
     case constr_app ctr_name args_rev₁ args_rev₁' hlen₁ ch₁ =>
@@ -204,17 +205,17 @@ lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂
           contradiction
   | succ n ih =>
     intros k hk h₁ h₂
-    cases h₁.invert
+    invert h₁
     case unit =>
-      cases h₂.invert
+      invert h₂
       case unit =>
         exact Value.Approx.Indexed.unit
     case const =>
-      cases h₂.invert
+      invert h₂
       case const =>
         exact Value.Approx.Indexed.const
     case constr_app ctr_name args_rev args_rev' hlen₁ ch₁ =>
-      cases h₂.invert
+      invert h₂
       case constr_app args_rev'' hlen₂ ch₂ =>
         apply Value.Approx.Indexed.constr_app
         · aesop
@@ -223,7 +224,7 @@ lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲(n) v₂ → v₂
           have : k' ≤ n := by linarith
           aesop
     case closure env₁ body₁ env₂ body₂ ch₁ =>
-      cases h₂.invert
+      invert h₂
       case closure env₃ body₃ ch₂ =>
         apply Value.Approx.Indexed.closure
         · intro n₁ n₂ hn a₁ a₃ v₁ happrox heval₁
@@ -258,7 +259,6 @@ lemma Value.Approx.const_refl {c} : Value.const c ≲ Value.const c := by
   intro
   exact Indexed.const
 
-@[trans]
 lemma Value.Approx.trans {v₁ v₂ v₃} : v₁ ≲ v₂ → v₂ ≲ v₃ → v₁ ≲ v₃ := by
   intros h₁ h₂
   intro n
@@ -269,7 +269,7 @@ lemma Value.Approx.unit_left {v} : v ≲ Value.unit ↔ v = Value.unit := by
   constructor
   case mp =>
     intro h
-    cases (h 0).invert
+    invert (h 0)
     rfl
   case mpr =>
     intro h
@@ -281,7 +281,7 @@ lemma Value.Approx.unit_right {v} : Value.unit ≲ v ↔ v = Value.unit := by
   constructor
   case mp =>
     intro h
-    cases (h 0).invert
+    invert (h 0)
     rfl
   case mpr =>
     intro h
@@ -293,7 +293,7 @@ lemma Value.Approx.const_left {v c} : v ≲ Value.const c ↔ v = Value.const c
   constructor
   case mp =>
     intro h
-    cases (h 0).invert
+    invert (h 0)
     rfl
   case mpr =>
     intro h
@@ -305,7 +305,7 @@ lemma Value.Approx.const_right {v c} : Value.const c ≲ v ↔ v = Value.const c
   constructor
   case mp =>
     intro h
-    cases (h 0).invert
+    invert (h 0)
     rfl
   case mpr =>
     intro h
@@ -320,7 +320,6 @@ lemma Value.Approx.constr_app {ctr_name args_rev args_rev'} :
   intro hlen h n
   aesop
 
-@[aesop unsafe apply]
 lemma Value.Approx.closure {env₁ body₁ env₂ body₂} :
   (∀ a₁ a₂,
     a₁ ≲ a₂ →
@@ -338,10 +337,10 @@ lemma Value.Approx.constr_app_inv {ctr_name args_rev args_rev'} :
   constructor
   case left =>
     intros p hp n
-    cases (h (n + 1)).invert
+    invert (h (n + 1))
     aesop
   case right =>
-    cases (h 0).invert
+    invert (h 0)
     aesop
 
 lemma Value.Approx.constr_app_inv_length {ctr_name args_rev args_rev'} :
@@ -364,7 +363,7 @@ lemma Value.Approx.constr_app_inv_left {ctr_name args_rev' v} :
     args_rev.length = args_rev'.length ∧
     ∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p := by
   intro h
-  cases (h 0).invert
+  invert (h 0)
   aesop
 
 @[aesop unsafe 90% destruct]
@@ -375,7 +374,7 @@ lemma Value.Approx.constr_app_inv_right {ctr_name args_rev v} :
     args_rev.length = args_rev'.length ∧
     ∀ p ∈ List.zip args_rev args_rev', Prod.fst p ≲ Prod.snd p := by
   intro h
-  cases (h 0).invert
+  invert (h 0)
   aesop
 
 @[aesop safe destruct (immediate := [h])]
@@ -394,9 +393,14 @@ lemma Value.Approx.closure_inv {env₁ body₁ env₂ body₂}
         apply Eval.deterministic <;> assumption
       subst this
       simp_all only
-  intro n
-  cases (h n.succ).invert
-  sorry
+  intro n₂
+  obtain ⟨n₁, h''⟩ := Eval.toIndexed h'
+  invert (h (n₁ + n₂ + 1))
+  case closure ch =>
+    apply ch (n₁ := n₁) (n₂ := n₂)
+    · linarith
+    · apply ha
+    · assumption
 
 @[aesop unsafe 90% destruct]
 lemma Value.Approx.closure_inv_left {env₂ body₂ v} :
@@ -405,7 +409,7 @@ lemma Value.Approx.closure_inv_left {env₂ body₂ v} :
     v = Value.closure env₁ body₁ ∧
     (∀ a₁ a₂, a₁ ≲ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) := by
   intro h
-  cases (h 0).invert
+  invert (h 0)
   aesop
 
 @[aesop unsafe 90% destruct]
@@ -415,7 +419,7 @@ lemma Value.Approx.closure_inv_right {env₁ body₁ v} :
     v = Value.closure env₂ body₂ ∧
     (∀ a₁ a₂, a₁ ≲ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) := by
   intro h
-  cases (h 0).invert
+  invert (h 0)
   aesop
 
 @[aesop safe cases]
@@ -436,14 +440,13 @@ lemma Value.Approx.invert {v v'} :
   v ≲ v' →
   Value.Approx.Inversion v v' := by
   intro h
-  cases (h 0).invert <;> constructor <;> aesop
+  invert (h 0) <;> constructor <;> aesop
 
 @[refl]
 lemma Expr.Approx.refl {env} e : e ≲⟨env, env⟩ e := by
   intro v
   aesop
 
-@[trans]
 lemma Expr.Approx.trans {env₁ env₂ env₃ e₁ e₂ e₃} :
   e₁ ≲⟨env₁, env₂⟩ e₂ → e₂ ≲⟨env₂, env₃⟩ e₃ → e₁ ≲⟨env₁, env₃⟩ e₃ := by
   intros h₁ h₂ v₁ heval₁
@@ -452,6 +455,6 @@ lemma Expr.Approx.trans {env₁ env₂ env₃ e₁ e₂ e₃} :
   exists v₃
   constructor
   · assumption
-  · trans <;> assumption
+  · exact Value.Approx.trans happrox₂ happrox₃
 
 end Juvix.Core.Main