Skip to content

Commit 1f27d0a

Browse files
FrederickPuFrederickPu
committed
made progress on assign proof
1 parent 32cc211 commit 1f27d0a

1 file changed

Lines changed: 119 additions & 39 deletions

File tree

‎Pullback/UnquoteTy/SSA.lean‎

Lines changed: 119 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Lean
22
import Mathlib.Logic.ExistsUnique
3-
import Std.Tactic.Do
3+
import Mathlib.Data.Fin.Tuple.Basic
44

55
open Lean
66

@@ -79,6 +79,10 @@ Fin.last' - Fin.cast (size_reverse) res) (as.reverse.findFinIdx? p)
7979
def VarMap.get (map : VarMap) (key : Name) : Option SSAType :=
8080
map.findLast? (·.1 = key) |>.map (·.2)
8181

82+
theorem VarMap.get_push (vars : VarMap) (last : Name × SSAType) (key : Name) : (cast (β := VarMap) rfl (vars.push last)).get key = if last.1 = key then some last.2 else vars.get key := sorry
83+
84+
theorem VarMap.get_eq_some_iff_any (vars : VarMap) (key : Name) (a : SSAType) : vars.get key = some a ↔ vars.any (·.1 = key) := sorry
85+
8286
def SSAConst.inferType : SSAConst → SSAType
8387
| ofFloat _ => .ofBase .float
8488
| ofInt _ => .ofBase .int
@@ -300,6 +304,23 @@ def mkMutTuple : VarMap → SSAExpr × SSAType
300304
(.app (.app (.const (.prod type rightType)) (.var name)) rightExpr, .prod type rightType)
301305
termination_by as => as.size
302306

307+
#check getElem
308+
#check Array.findFinIdx?_eq_some_iff
309+
-- #check Fin.find_eq_some_iff
310+
theorem SSAExpr.inferType_mkMutTuple (vars : VarMap) : (mutVars : VarMap) → (h : mutVars.toList ⊆ vars.toList) → (h' : ∀ x ∈ mutVars.toList, ∃! y ∈ vars.toList, x.1 = y.1) → (mkMutTuple mutVars).fst.inferType vars = (mkMutTuple mutVars).snd
311+
| ⟨[]⟩ => by simp [inferType, mkMutTuple, SSAConst.inferType]
312+
| ⟨[(name, type)]⟩ => by
313+
simp [inferType, mkMutTuple, VarMap.get]
314+
intro h ⟨i, hi, H⟩
315+
obtain ⟨hi, hhi⟩ := hi
316+
sorry
317+
| ⟨(name, type)::b::l⟩ => by
318+
intro h h'
319+
simp at h'
320+
simp [mkMutTuple]
321+
sorry
322+
termination_by as => as.size
323+
303324
def destructMutTuple (tupleName : Name) : VarMap → SSAExpr → SSAExpr
304325
| ⟨[]⟩, body => body
305326
| ⟨[(name, _)]⟩, body => .letE name (.var tupleName) body
@@ -381,7 +402,10 @@ def SSADo.toSSAExpr (vars : VarMap) (mutVars : VarMap) (kbreak kcontinue : Optio
381402
let valT ← val.inferType vars
382403
return SSAExpr.letE var val (← rest.toSSAExpr (vars.push (var, valT)) (mutVars.push (var, valT)) kbreak kcontinue)
383404
| assign var val rest => do
405+
let varT ← mutVars.get var
384406
let valT ← val.inferType vars
407+
if valT != varT then
408+
none
385409
return SSAExpr.letE var val (← rest.toSSAExpr (vars.push (var, valT)) mutVars kbreak kcontinue)
386410
| loop body rest => do
387411
let (mutTuple, mutTupleType) := (mkMutTuple mutVars)
@@ -452,7 +476,7 @@ theorem SSAExpr.welltyped_app_iff (vars : VarMap) (f x : SSAExpr) : ((f.app x).i
452476
/-
453477
name `k` referes to a valid continutation for the current mutvars
454478
-/
455-
def SSADo.validContinutation (vars : VarMap) (mutVars : VarMap) (k : Name) := (do pure <| (← vars.get k).funDom? = (mkMutTuple mutVars).2) = some true
479+
def SSADo.validContinutation (vars : VarMap) (mutVars : VarMap) (k : Name) := ¬ mutVars.any (·.1 = k) ∧ (do pure <| (← vars.get k).funDom? = (mkMutTuple mutVars).2) = some true
456480

457481
/-
458482
`k` is the name of a valid continuation or none
@@ -462,23 +486,9 @@ def SSADo.validContinutationRef (vars : VarMap) (mutVars : VarMap) (k : Option N
462486
| some k' => validContinutation vars mutVars k'
463487
| none => True
464488

465-
open Std Do
466-
/--
467-
Adequacy lemma for `Option`.
468-
Useful if you want to prove a property about a complex expression `prog : Option α` that you have
469-
generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
470-
-/
471-
theorem Std.Do.Option.of_wp_eq {α} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
472-
(⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
473-
subst h
474-
intro hspec
475-
simp only [wp, Id.run, PredTrans.pushOption_apply, PredTrans.pure_apply, SPred.entails_nil,
476-
SPred.down_pure] at hspec
477-
split at hspec <;> exact hspec True.intro
478-
479489
theorem SSAExpr.inferType_eq_of_hygenic (vars : VarMap) (newvar : Name) (newVarType : SSAType) (hHygenic : ¬ vars.any (·.1 = newvar)) (expr : SSAExpr) : (expr.inferType vars).isSome → expr.inferType (vars.push (newvar, newVarType)) = expr.inferType vars := sorry
480490

481-
theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kcontinue : Option Name) (hkBreak : validContinutationRef vars mutVars kbreak) (hkContinue : validContinutationRef vars mutVars kcontinue) (hMut₁ : (mutVars.toList.map (·.1)).Nodup) (hMut₂ : mutVars.toList ⊆ vars.toList) (hMut₃ : ∀ mutvar ∈ mutVars.toList, ∃! var ∈ vars.toList, var.1 = mutvar.1) : (prog : SSADo) → (hp : (prog.toSSAExpr vars mutVars kbreak kcontinue).isSome) → (((prog.toSSAExpr vars mutVars kbreak kcontinue).get hp).inferType vars).isSome
491+
theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kcontinue : Option Name) (hkBreak : validContinutationRef vars mutVars kbreak) (hkContinue : validContinutationRef vars mutVars kcontinue) (hMut₁ : (mutVars.toList.map (·.1)).Nodup) (hMut₂ : mutVars.toList ⊆ vars.toList) (hMut₃ : ∀ x ∈ mutVars.toList, ∃! y ∈ vars.toList, x.1 = y.1) : (prog : SSADo) → (hp : (prog.toSSAExpr vars mutVars kbreak kcontinue).isSome) → (((prog.toSSAExpr vars mutVars kbreak kcontinue).get hp).inferType vars).isSome
482492
| .expr e => by
483493
intro hp
484494
simp [toSSAExpr] at hp
@@ -487,7 +497,7 @@ theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kco
487497
match hkc : kcontinue with
488498
| some kc =>
489499
simp [validContinutationRef, validContinutation, Option.bind_eq_some_iff] at hkContinue
490-
obtain ⟨fkc, hfkc⟩ := hkContinue
500+
obtain ⟨_, fkc, hfkc⟩ := hkContinue
491501
have crux : (SSAExpr.inferType vars (mkMutTuple mutVars).fst) = (mkMutTuple mutVars).snd := sorry
492502
obtain ⟨β, hb⟩ : ∃ β, fkc = .fun (mkMutTuple mutVars).snd β := sorry
493503
simp [toSSAExpr, SSAExpr.inferType, crux, hfkc, hb]
@@ -498,44 +508,108 @@ theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kco
498508
match hv : mutVars.any (·.1 = var) with
499509
| false =>
500510
simp [toSSAExpr, hv, Option.isSome_iff_exists, Option.bind_eq_some_iff] at hp
501-
obtain ⟨a, varT, hvarT, a2, ha2⟩ := hp
502-
have := toSSAExpr_wellTyped (vars.push (var, varT)) mutVars kbreak kcontinue sorry sorry sorry sorry sorry rest (by simp [ha2.1])
511+
obtain ⟨varT, hvarT, a2, ha2⟩ := hp
512+
have := toSSAExpr_wellTyped (vars.push (var, varT)) mutVars kbreak kcontinue sorry sorry sorry sorry sorry rest (by simp [ha2])
503513
grind [toSSAExpr, SSAExpr.inferType, Option.isSome_iff_exists]
504514
| true =>
505515
simp [toSSAExpr, hv] at hp
506516
| .letM var val rest => by
507517
intro hp
508518
match hv : mutVars.any (·.1 = var) with
509519
| false =>
510-
simp [toSSAExpr, hv, Option.isSome_iff_exists, Option.bind_eq_some_iff] at hp
511-
obtain ⟨a, varT, hvarT, a2, ha2⟩ := hp
512-
have := toSSAExpr_wellTyped (vars.push (var, varT)) (mutVars.push (var, varT)) kbreak kcontinue sorry sorry sorry sorry sorry rest (by simp [ha2.1])
520+
simp only [toSSAExpr, hv, Bool.false_eq_true, ↓reduceIte, Option.pure_def,
521+
Option.bind_eq_bind, Option.bind_some, Option.isSome_iff_exists, Option.bind_eq_some_iff,
522+
Option.some.injEq, ↓existsAndEq, and_true, exists_and_left] at hp
523+
obtain ⟨varT, hvarT, a2, ha2⟩ := hp
524+
have := toSSAExpr_wellTyped (vars.push (var, varT)) (mutVars.push (var, varT)) kbreak kcontinue sorry sorry sorry sorry sorry rest (by simp [ha2])
513525
grind [toSSAExpr, SSAExpr.inferType, Option.isSome_iff_exists]
514526
| true =>
515527
simp [toSSAExpr, hv] at hp
516528
| .assign var val rest => by
517529
intro hp
518-
simp [toSSAExpr, Option.isSome_iff_exists, Option.bind_eq_some_iff] at hp
519-
obtain ⟨a, varT, hvarT, a2, ha2⟩ := hp
520-
have := toSSAExpr_wellTyped (vars.push ⟨var, varT⟩) mutVars kbreak kcontinue sorry sorry sorry sorry sorry rest (by grind)
521-
grind [toSSAExpr, SSAExpr.inferType, Option.isSome_iff_exists]
530+
simp only [toSSAExpr, bne_iff_ne, ne_eq, Option.pure_def, Option.bind_eq_bind, Option.bind_none,
531+
Option.bind_some, ite_not, Option.isSome_iff_exists, Option.bind_eq_some_iff,
532+
Option.ite_none_right_eq_some, Option.some.injEq, ↓existsAndEq, true_and, and_true,
533+
exists_and_left] at hp
534+
obtain ⟨varT, hvarT, HT, restExpr, hRestExpr⟩ := hp
535+
have := toSSAExpr_wellTyped (vars.push ⟨var, varT⟩) mutVars kbreak kcontinue (by {
536+
cases hkb : kbreak with
537+
| some kbreak' =>
538+
simp only [validContinutationRef, validContinutation, Option.pure_def, Option.bind_eq_bind]
539+
have := VarMap.get_push vars (var, varT) kbreak'
540+
simp only [cast_eq] at this
541+
simp [this]
542+
simp [validContinutationRef, hkb] at hkBreak
543+
have : var ≠ kbreak' := by
544+
intro hh
545+
rw [hh, VarMap.get_eq_some_iff_any] at hvarT
546+
have := hkBreak.1
547+
rw [← hh] at this
548+
grind
549+
simp [this]
550+
simp [validContinutation] at hkBreak
551+
grind
552+
| none => simp only [validContinutationRef]
553+
}) (by {
554+
cases hkb : kcontinue with
555+
| some kbreak' =>
556+
simp only [validContinutationRef, validContinutation, Option.pure_def, Option.bind_eq_bind]
557+
have := VarMap.get_push vars (var, varT) kbreak'
558+
simp only [cast_eq] at this
559+
simp [this]
560+
simp [validContinutationRef, hkb] at hkContinue
561+
have : var ≠ kbreak' := by
562+
intro hh
563+
rw [hh, VarMap.get_eq_some_iff_any] at hvarT
564+
have := hkContinue.1
565+
rw [← hh] at this
566+
grind
567+
simp [this]
568+
simp [validContinutation] at hkContinue
569+
grind
570+
| none => simp only [validContinutationRef]
571+
}) (by grind) (by grind) (by {
572+
intro x hx
573+
specialize hMut₃ x hx
574+
obtain ⟨y, hy, Hy⟩ := hMut₃
575+
use y
576+
use (by grind)
577+
intro y'
578+
simp only [Array.toList_push, List.mem_append, Array.mem_toList_iff, List.mem_cons,
579+
List.not_mem_nil, or_false, and_imp]
580+
intro h1 h2
581+
cases h1 with
582+
| inl hl =>
583+
exact Hy y' (by grind)
584+
| inr hr =>
585+
specialize Hy x (by grind)
586+
have : x.2 = varT := by {
587+
have : ∀ z ∈ mutVars.toList, z.1 = x.1 → z = x := by
588+
sorry
589+
specialize this (var, varT) (by sorry)
590+
grind
591+
}
592+
grind
593+
}) rest (by grind)
594+
simp only [toSSAExpr, hvarT, HT, bne_iff_ne, ne_eq, Option.pure_def, Option.bind_eq_bind,
595+
Option.bind_none, Option.bind_some, ite_not, ↓reduceIte, Option.get_bind, Option.get_some,
596+
SSAExpr.inferType, this]
522597
| .break => by
523598
intro hp
524599
match kbreak with
525600
| some kbreak' =>
526601
simp [toSSAExpr, Option.isSome_iff_exists] at hp
527-
have : (mkMutTuple mutVars).fst.inferType vars = (mkMutTuple mutVars).snd := sorry
528-
simp [toSSAExpr]
602+
have : (mkMutTuple mutVars).fst.inferType vars = (mkMutTuple mutVars).snd := SSAExpr.inferType_mkMutTuple _ _ hMut₂ hMut₃
603+
simp only [toSSAExpr, Option.bind_eq_bind, Option.bind_some]
529604
grind [toSSAExpr, validContinutationRef, validContinutation, toSSAExpr, SSAExpr.welltyped_app_iff, SSAExpr.inferType, Option.isSome_iff_exists]
530605
| none =>
531606
simp [toSSAExpr] at hp
532607
| .continue => by
533608
intro hp
534609
match kcontinue with
535610
| some kcontinue' =>
536-
simp [toSSAExpr, Option.isSome_iff_exists] at hp
537-
have : (mkMutTuple mutVars).fst.inferType vars = (mkMutTuple mutVars).snd := sorry
538-
simp [toSSAExpr]
611+
have : (mkMutTuple mutVars).fst.inferType vars = (mkMutTuple mutVars).snd := SSAExpr.inferType_mkMutTuple _ _ hMut₂ hMut₃
612+
simp only [toSSAExpr, Option.bind_eq_bind, Option.bind_some]
539613
grind [toSSAExpr, validContinutationRef, validContinutation, toSSAExpr, SSAExpr.welltyped_app_iff, SSAExpr.inferType, Option.isSome_iff_exists]
540614
| none =>
541615
simp [toSSAExpr] at hp
@@ -544,14 +618,20 @@ theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kco
544618
grind [toSSAExpr, Option.isSome_iff_exists, Option.bind_eq_some_iff]
545619
| .ifthenelse c t e rest => by
546620
intro hp
547-
simp [toSSAExpr, Option.isSome_iff_exists, Option.bind_eq_some_iff] at hp
548-
obtain ⟨_, restExpr, hRestExpr, cType, hcType, hcType', tExpr, htExpr, tExprType, htExprType, eExpr, heExpr, eExprType, heExprType, heq, _⟩ := hp
621+
simp only [toSSAExpr, Array.append_eq_append, bne_iff_ne, ne_eq, Option.bind_eq_bind,
622+
Option.bind_none, Option.pure_def, Option.bind_some, ite_not, Option.isSome_iff_exists,
623+
Option.bind_eq_some_iff, Option.ite_none_right_eq_some, Option.some.injEq, ↓existsAndEq,
624+
true_and, and_true, exists_and_left, exists_and_right] at hp
625+
obtain ⟨⟨restExpr, hRestExpr⟩, hctype, tExpr, htExpr, tExprType, htExprType, eExpr, heExpr, heType⟩ := hp
549626
let restMutVars : Array Name := rest.collectMutVars
550627
let nS : Name := freshName (Array.append (mutVars.map (·.1)) restMutVars) `s
551-
have crux := toSSAExpr_wellTyped (vars.push (nS, (mkMutTuple mutVars).2)) mutVars kbreak kcontinue sorry sorry sorry sorry sorry rest (by simp [hRestExpr, nS, restMutVars])
628+
have crux := toSSAExpr_wellTyped (vars.push (nS, (mkMutTuple mutVars).2)) mutVars kbreak kcontinue sorry sorry sorry sorry sorry rest (by {
629+
simp [restMutVars, nS]
630+
grind
631+
})
552632
simp [nS, restMutVars, hRestExpr, Option.isSome_iff_exists] at crux
553633
obtain ⟨restExprType, hRestExprType⟩ := crux
554-
simp [toSSAExpr, SSAExpr.inferType, hcType, hcType', hRestExpr, htExpr, htExprType, heExpr, heExprType]
634+
simp [toSSAExpr, SSAExpr.inferType, hctype, hRestExpr, htExpr, htExprType, heExpr, heType]
555635
have : (SSAExpr.inferType
556636
(Array.push vars
557637
(freshName (Array.map (fun x => x.fst) mutVars ++ rest.collectMutVars) `s, (mkMutTuple mutVars).snd))
@@ -565,8 +645,8 @@ theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kco
565645
c) = SSAExpr.inferType vars c := by
566646
apply SSAExpr.inferType_eq_of_hygenic
567647
sorry
568-
simp [hcType]
569-
simp [this, hcType, SSAConst.inferType, hcType']
648+
simp [hctype]
649+
simp [this, hctype, SSAConst.inferType]
570650
have : (SSAExpr.inferType
571651
(Array.push vars
572652
(freshName (Array.map (fun x => x.fst) mutVars) `kcontinue, (mkMutTuple mutVars).snd.fun restExprType))
@@ -576,7 +656,7 @@ theorem SSADo.toSSAExpr_wellTyped (vars : VarMap) (mutVars : VarMap) (kbreak kco
576656
(Array.push vars
577657
(freshName (Array.map (fun x => x.fst) mutVars) `kcontinue, (mkMutTuple mutVars).snd.fun restExprType))
578658
eExpr) = SSAExpr.inferType vars eExpr := sorry
579-
simp [this, heExprType, heq]
659+
simp [this, heType]
580660
| _ => sorry
581661

582662
#check SSADo

0 commit comments

Comments
 (0)