made progress towards toSSAExpr!_vars_equiv

Author: FrederickPu

Pullback/SSA/SSADo.lean

@@ -247,25 +247,97 @@ theorem SSADo.eval_letM
         (rest.toSSAExpr! (vars.push (var, val.inferType! vars)) (mutVars.push (var, val.inferType! vars)) kMutVars kbreak kcontinue)
         v hval
 
-theorem SSADo.eval_toSSAExpr_push_assign_invariant
+
+#check SSADo.toSSAExpr!
+theorem SSADo.toSSAExpr!_vars_equiv
+    {vars₁ vars₂ mutVars kMutVars : VarMap} {kbreak kcontinue : Option Name}
+    (hvars : VarMap.equiv vars₁ vars₂) :
+    {rest : SSADo} →
+    (rest.toSSAExpr! vars₁ mutVars kMutVars kbreak kcontinue) =
+    (rest.toSSAExpr! vars₂ mutVars kMutVars kbreak kcontinue)
+| expr x => by
+    simp [toSSAExpr!]
+| letE varName val body => by
+    simp only [toSSAExpr!, SSAExpr.letE.injEq, true_and]
+    apply SSADo.toSSAExpr!_vars_equiv
+    have : SSAExpr.inferType! vars₁ val = SSAExpr.inferType! vars₂ val :=
+      SSAExpr.inferType!_eq_of_vars_equiv hvars
+    rw [this]
+    exact VarMap.equiv_push vars₁ vars₂ hvars varName (SSAExpr.inferType! vars₂ val)
+| letM varName val body => by
+    simp only [toSSAExpr!, SSAExpr.letE.injEq, true_and]
+    have : SSAExpr.inferType! vars₁ val = SSAExpr.inferType! vars₂ val :=
+      SSAExpr.inferType!_eq_of_vars_equiv hvars
+    rw [this]
+    apply toSSAExpr!_vars_equiv
+    exact VarMap.equiv_push vars₁ vars₂ hvars varName (SSAExpr.inferType! vars₂ val)
+| assign varname val body => by
+    simp [toSSAExpr!]
+    apply SSADo.toSSAExpr!_vars_equiv
+    have : SSAExpr.inferType! vars₁ val = SSAExpr.inferType! vars₂ val :=
+      SSAExpr.inferType!_eq_of_vars_equiv hvars
+    rw [this]
+    exact VarMap.equiv_push vars₁ vars₂ hvars varname (SSAExpr.inferType! vars₂ val)
+| .return out => by simp [toSSAExpr!]
+| .break => by simp [toSSAExpr!]
+| .continue => by simp [toSSAExpr!]
+| seq s₁ s₂ => by
+    simp [toSSAExpr!]
+    apply And.intro
+    · exact toSSAExpr!_vars_equiv hvars
+    · exact toSSAExpr!_vars_equiv hvars
+| loop body rest => by
+    simp [toSSAExpr!]
+    have : freshName (Array.map (fun x => x.1) vars₁ ++ body.vars) =
+    freshName (Array.map (fun x => x.1) vars₂ ++ body.vars) := sorry
+    simp [this]
+    simp [toSSAExpr!_vars_equiv hvars, SSAExpr.inferType!_eq_of_vars_equiv hvars]
+| ifthenelse c t e rest => by
+    simp [toSSAExpr!]
+    have : freshName (Array.map (fun x => x.1) vars₁ ++ (t.vars ++ e.vars)) =
+    freshName (Array.map (fun x => x.1) vars₂ ++ (t.vars ++ e.vars)) := sorry
+    simp [this]
+    simp [toSSAExpr!_vars_equiv hvars, SSAExpr.inferType!_eq_of_vars_equiv hvars]
+    -- rw [toSSAExpr!_vars_equiv (vars₂ := vars₂), SSAExpr.inferType!_eq_of_vars_equiv (vars₂ := vars₂)]
+    -- apply And.intro
+    sorry
+
+theorem SSADo.toSSAExpr_var_push
     {vars mutVars kMutVars : VarMap} {kbreak kcontinue : Option Name}
-    {args : Array (Name × SSAConst)}
     {var : Name} {val : SSAExpr} {rest : SSADo} :
-    (rest.toSSAExpr! (vars.push (var, val.inferType! vars)) mutVars kMutVars kbreak kcontinue).eval args =
-    (rest.toSSAExpr! vars mutVars kMutVars kbreak kcontinue).eval args := by
-    sorry
+    (hvar_type : vars.get var = some (val.inferType! vars)) →
+    (rest.toSSAExpr! (vars.push (var, val.inferType! vars)) mutVars kMutVars kbreak kcontinue) =
+    (rest.toSSAExpr! vars mutVars kMutVars kbreak kcontinue) := by
+    intro hvar_type
+    have hpush_equiv : VarMap.equiv (vars.push (var, val.inferType! vars)) vars := by
+        apply VarMap.equiv_symm
+        apply  VarMap.equiv_push_of_shadow
+        grind
+    simpa using SSADo.toSSAExpr!_vars_equiv
+        (vars₁ := (vars.push (var, val.inferType! vars)))
+        (vars₂ := vars)
+        (mutVars := mutVars)
+        (kMutVars := kMutVars)
+        (kbreak := kbreak)
+        (kcontinue := kcontinue)
+        (rest := rest)
+        hpush_equiv
 
 theorem SSADo.eval_assign
     {vars mutVars kMutVars : VarMap} {kbreak kcontinue : Option Name}
     {args : Array (Name × SSAConst)}
     {var : Name} {val : SSAExpr} {rest : SSADo} {v : SSAConst}
+    (hvar_type : vars.get var = some (val.inferType! vars))
     (_hval : val.eval args = some v) :
     (SSADo.toSSAExpr! vars mutVars kMutVars kbreak kcontinue (SSADo.assign var val rest)).eval args =
             (SSADo.toSSAExpr! vars mutVars kMutVars kbreak kcontinue rest).eval args := by
     have hassign_bridge :
             (rest.toSSAExpr! (vars.push (var, val.inferType! vars)) mutVars kMutVars kbreak kcontinue).eval args =
             (rest.toSSAExpr! vars mutVars kMutVars kbreak kcontinue).eval args := by
-        exact SSADo.eval_toSSAExpr_push_assign_invariant
+        exact congrArg (fun e => e.eval args) <|
+            SSADo.toSSAExpr_var_push (vars := vars) (mutVars := mutVars) (kMutVars := kMutVars)
+                (kbreak := kbreak) (kcontinue := kcontinue) (var := var) (val := val)
+                (rest := rest) hvar_type
     have hlet :
             (SSADo.toSSAExpr! vars mutVars kMutVars kbreak kcontinue (SSADo.assign var val rest)).eval args =
             (rest.toSSAExpr! (vars.push (var, val.inferType! vars)) mutVars kMutVars kbreak kcontinue).eval args := by

Pullback/SSA/VarMap.lean

@@ -28,16 +28,25 @@ theorem VarMap.get_eq_none_iff_not_any (vars : VarMap) (key : Name) : vars.get k
 def VarMap.equiv (vars₁ vars₂ : VarMap) : Prop :=
     {name | vars₁.any (·.1 = name)} = {name | vars₂.any (·.1 = name)} ∧ ∀ name, vars₁.any (·.1 = name) → vars₁.get name = vars₂.get name
 
-def VarMap.equiv_push (vars₁ vars₂ : VarMap) (hvars : vars₁.equiv vars₂) (varname : Name) (vartype : SSAType) : (cast (β := VarMap) rfl (vars₁.push (varname, vartype))).equiv (vars₂.push (varname, vartype)) := by
-    simp only [cast_eq]
+def VarMap.equiv_symm {vars₁ vars₂ : VarMap} : vars₁.equiv vars₂ → vars₂.equiv vars₁ := by
+    simp only [equiv, Array.any_eq_true', decide_eq_true_eq, forall_exists_index, and_imp]
+    intro h1 h2
+    have : ∀ (name : Name) (x : Name × SSAType), x ∈ vars₂ → x.1 = name → Array.get vars₂ name = Array.get vars₁ name := by
+        intro name a ha1 ha2
+        rw [Set.ext_iff] at h1
+        specialize h1 a.1
+        grind
+    tauto
+
+def VarMap.equiv_push (vars₁ vars₂ : VarMap) (hvars : vars₁.equiv vars₂) (varname : Name) (vartype : SSAType) : VarMap.equiv (vars₁.push (varname, vartype)) (vars₂.push (varname, vartype)) := by
     simp only [equiv, Array.any_eq_true, decide_eq_true_eq, forall_exists_index, Array.size_push, Array.any_push', Bool.or_eq_true] at ⊢ hvars
     apply And.intro
     · ext name
       rw [Set.ext_iff] at hvars
       grind only [usr Set.mem_setOf_eq]
     · intro name H
       have := VarMap.get_push
-      simp only [cast_eq, Prod.forall] at this
+      simp only [Prod.forall] at this
       rw [this]
       cases em (varname = name) with
       | inl hl =>
@@ -50,6 +59,8 @@ def VarMap.equiv_push (vars₁ vars₂ : VarMap) (hvars : vars₁.equiv vars₂)
         simp [hr]
         grind only
 
+def VarMap.equiv_push_of_shadow (vars : VarMap) (varname : Name) (vartype : SSAType) (hvar_type : vars.get varname = some vartype): VarMap.equiv vars (vars.push (varname, vartype)) := sorry
+
 theorem SSAExpr.inferType_eq_of_vars_equiv (vars₁ vars₂ : VarMap) (hvars : vars₁.equiv vars₂) : (expr : SSAExpr) → expr.inferType vars₁ = expr.inferType vars₂
 | const c => by simp only [inferType]
 | letE varname val body => by
@@ -120,3 +131,8 @@ theorem VarMap.push_valid {var : Name} {varT : SSAType} {mutVars vars : VarMap}
         grind
     have : Array.get vars var = varT := by grind
     grind
+
+theorem SSAExpr.inferType!_eq_of_vars_equiv {vars₁ vars₂ : VarMap} (hvars : VarMap.equiv vars₁ vars₂) {expr : SSAExpr} :
+    expr.inferType! vars₁ = expr.inferType! vars₂ := sorry
+
+#check mkMutTuple