Fill-in proof for ProgramWF

Strata/Languages/Boogie/ProcedureWF.lean

@@ -29,6 +29,9 @@ theorem snd_values_mem {ps : ListMap BoogieLabel Procedure.Check} :
     case inr mem => right ; exact (ih mem)
   case nil => cases Hin
 
+theorem Procedure.typeCheckWF : Procedure.typeCheck T p pp = Except.ok (pp', T') → WFProcedureProp p pp := by sorry
+
+
 /-
 set_option warn.sorry false in
 /--

Strata/Languages/Boogie/ProgramWF.lean

@@ -215,6 +215,41 @@ theorem Program.typeCheck.goWF' :
           refine ⟨_, _, _, heq⟩
 -/
 
+
+theorem Program.find?.go_none_of_append : Program.find?.go kind name (acc1 ++ acc2) = none → Program.find?.go kind name acc1 = none := by
+  induction acc1 <;> simp [Program.find?.go]
+  rename_i h t ind
+  split <;> simp_all
+
+theorem Program.typeCheck.go_elim_acc:
+  (Program.typeCheck.go p T ds (acc1 ++ acc2) = Except.ok (pp, T') →
+  (List.IsPrefix acc2.reverse pp ∧ Program.typeCheck.go p T ds acc1 = Except.ok (pp.drop acc2.length, T')))
+  := by
+  induction ds generalizing pp acc1 T
+  simp [Program.typeCheck.go]
+  intro  H
+  simp [← H]
+  rename_i h t ind
+  simp [Program.typeCheck.go]
+  simp [bind, Except.bind]
+  split <;> try contradiction
+  any_goals (split <;> try contradiction)
+  any_goals (split <;> try contradiction)
+  any_goals (split <;> try contradiction)
+  any_goals (split <;> try contradiction)
+  any_goals (split <;> try contradiction)
+  any_goals simp
+  any_goals (rw [List.cons_append_assoc]; intro; apply ind (by assumption))
+  any_goals (rename_i H _ _ _ _; have H:= Program.find?.go_none_of_append H; simp_all)
+  rename_i H _ _ _ _ _ _ _; have H:= Program.find?.go_none_of_append H; simp_all
+
+theorem Program.typeCheckAux_elim_singleton: Program.typeCheck.go p ds T [s] = Except.ok (pp, T') →
+  Program.typeCheck.go p ds T [] = Except.ok (pp.drop 1, T') := by
+  intro H
+  have : [s] = [] ++ [s] := by simp
+  rw [this] at H; have H:=  Program.typeCheck.go_elim_acc H
+  simp [H]
+
 /--
 Auxiliary lemma for Program.typeCheckWF
 -/
@@ -224,15 +259,20 @@ theorem Program.typeCheck.goWF : Program.typeCheck.go p T ds [] = .ok (ds', T')
   | nil => simp [Program.typeCheck.go] at tcok
            cases tcok; constructor <;> try assumption
   | cons h t t_ih =>
-    apply (List.Forall_cons (WF.WFDeclProp p) h t).mpr
+    simp [Program.typeCheck.go, bind, Except.bind] at tcok
+    split at tcok <;> try contradiction
+    any_goals (split at tcok <;> try contradiction)
+    any_goals (split at tcok <;> try contradiction)
+    any_goals (split at tcok <;> try contradiction)
+    any_goals (split at tcok <;> try contradiction)
+    simp
+    any_goals simp [t_ih $ Program.typeCheckAux_elim_singleton tcok]
+    have := Statement.typeCheckWF (by assumption)
     constructor
-    . sorry
-      -- apply (Program.typeCheck.goWF' tcok).1
-    . -- have H := (Program.typeCheck.goWF' tcok).2
-      -- cases H with | intro ds'' H => cases H with | intro TT H =>
-      -- cases H with
-      -- | intro TT' H => exact t_ih H
-      sorry
+    simp [WFCmdExtProp] at this
+    sorry
+    any_goals (apply Procedure.typeCheckWF (by assumption))
+    any_goals constructor
 
 /--
 The main lemma stating that a program 'p' that passes type checking is well formed

Strata/Languages/Boogie/StatementWF.lean

@@ -17,13 +17,51 @@ namespace WF
 
 open Std Lambda
 
+theorem typeCheckCmdWF: Statement.typeCheckCmd T p c = Except.ok v
+  → WFCmdExtProp p c := by
+  intro H
+  simp [Statement.typeCheckCmd, bind, Except.bind] at H
+  split at H <;> try contradiction
+  split at H <;> try contradiction
+  rename_i H' ; simp [Imperative.Cmd.typeCheck, bind, Except.bind] at H'
+  repeat (first | (split at H' <;> try contradiction) | constructor)
+  any_goals repeat (split at H <;> try contradiction)
+  any_goals simp_all
+  sorry
+  sorry
+  sorry
+
+theorem Statement.typeCheckAux_elim_acc: Statement.typeCheckAux.go p proc T ss (acc1 ++ acc2) = Except.ok (pp, T') ↔
+  (List.IsPrefix acc2.reverse pp ∧ Statement.typeCheckAux.go p proc T ss acc1 = Except.ok (pp.drop acc2.length, T'))
+  := by
+  induction ss generalizing pp acc1 acc2 T
+  simp [Statement.typeCheckAux.go]
+  constructor <;> intro H
+  simp [← H]
+  simp [H]
+  rw [← List.length_reverse, ← List.prefix_iff_eq_append]; simp [H]
+  rename_i h t ind
+  unfold Statement.typeCheckAux.go
+  simp [bind, Except.bind]
+  split <;> try contradiction
+  repeat (any_goals (split <;> try contradiction))
+  any_goals simp
+  any_goals rw [← List.cons_append, ind]
+
+theorem Statement.typeCheckAux_elim_singleton: Statement.typeCheckAux.go p proc T ss [s] = Except.ok (pp, T') →
+  Statement.typeCheckAux.go p proc T ss [] = Except.ok (pp.drop 1, T') := by
+  intro H
+  have : [s] = [] ++ [s] := by simp
+  rw [this, Statement.typeCheckAux_elim_acc] at H; simp at H
+  simp [H]
+
 theorem Statement.typeCheckAux_go_WF :
-  Statement.typeCheckAux.go p proc T ss acc = Except.ok (pp', T') →
+  Statement.typeCheckAux.go p proc T ss [] = Except.ok (pp', T') →
   WF.WFStatementsProp p acc →
   WF.WFStatementsProp p (acc ++ ss) := by
   intros tcok h_acc_ok
   induction ss generalizing acc T pp' T' with
-  | nil => simp_all
+  | nil => simp_all [WFStatementsProp]
   | cons h t ih =>
     unfold Statement.typeCheckAux.go at tcok
     simp [bind] at tcok
@@ -32,28 +70,75 @@ theorem Statement.typeCheckAux_go_WF :
       cases c with
       | call lhs procName args md =>
         -- Show that the called procedure is declared.
-        sorry
+        simp [Except.bind] at tcok
+        split at tcok <;> try contradiction
+        rw[List.append_cons];
+        have tcok := Statement.typeCheckAux_elim_singleton tcok
+        apply ih tcok <;> try assumption
+        simp [WFStatementsProp] at *
+        simp [List.Forall_append, Forall, *]
+        apply typeCheckCmdWF (by assumption)
       | cmd cmd =>
         simp [Except.bind] at tcok
-        split at tcok <;> try simp_all
-        sorry
-    | block label bss md => sorry
-    | ite c t e md => sorry
-    | goto l => sorry
-    | loop g m i b md => sorry
+        split at tcok <;> try contradiction
+        rw[List.append_cons];
+        have tcok := Statement.typeCheckAux_elim_singleton tcok
+        apply ih tcok <;> try assumption
+        simp [WFStatementsProp] at *
+        simp [List.Forall_append, Forall, *]
+        apply typeCheckCmdWF (by assumption)
+    | block label bss md =>
+      simp [Except.bind] at tcok
+      split at tcok <;> try contradiction
+      have tcok := Statement.typeCheckAux_elim_singleton tcok
+      rw[List.append_cons];
+      apply ih tcok <;> try assumption
+      simp [WFStatementsProp] at *
+      simp [List.Forall_append, Forall, *]
+      constructor
+    | ite c t e md =>
+      simp [Except.bind] at tcok
+      repeat (split at tcok <;> try contradiction)
+      have tcok := Statement.typeCheckAux_elim_singleton tcok
+      rw[List.append_cons];
+      apply ih tcok <;> try assumption
+      simp [WFStatementsProp] at *
+      simp [List.Forall_append, Forall, *]
+      constructor
+    | goto l =>
+      simp [Except.bind] at tcok
+      split at tcok <;> try contradiction
+      split at tcok <;> try contradiction
+      have tcok := Statement.typeCheckAux_elim_singleton tcok
+      rw[List.append_cons];
+      apply ih tcok <;> try assumption
+      simp [WFStatementsProp] at *
+      simp [List.Forall_append, Forall, *]
+      constructor
+    | loop g m i b md =>
+      simp [Except.bind] at tcok
+      repeat (split at tcok <;> try contradiction)
+      any_goals (repeat (split at tcok <;> try contradiction))
+      any_goals (repeat (split at tcok <;> try contradiction))
+      any_goals (repeat (split at tcok <;> try contradiction))
+      any_goals (have tcok := Statement.typeCheckAux_elim_singleton tcok; rw[List.append_cons])
+      any_goals (apply ih tcok <;> try assumption)
+      any_goals (try simp [WFStatementsProp] at *; try simp [List.Forall_append, *]; try constructor)
+      any_goals (simp [Forall])
+      any_goals constructor
 
 /--
 A list of Statement `ss` that passes type checking is well formed with respect
 to the whole program `p`.
 -/
-theorem Statement.typeCheckAuxWF :
+theorem Statement.typeCheckWF :
   Statement.typeCheck T p proc ss = Except.ok (pp', T') →
   WF.WFStatementsProp p ss := by
   intros tcok
   simp [Statement.typeCheck, Statement.typeCheckAux, bind, Except.bind] at tcok
   split at tcok <;> simp_all
   rename_i x v heq
-  have h_tc_go := @Statement.typeCheckAux_go_WF p proc T ss [] v.fst v.snd
+  have h_tc_go := @Statement.typeCheckAux_go_WF p proc T ss v.fst v.snd []
   simp_all [WFStatementsProp, Forall]
   done