From Undecidability.TM Require Import ProgrammingTools.
From Undecidability Require Import Hoare.HoareLogic Hoare.HoareCombinators Hoare.HoareRegister Hoare.HoareTactics Hoare.HoareTacticsView.
From Undecidability Require Import CaseNat.
From Coq Require Import ArithRing.
Arguments mult : simpl never.
Arguments plus : simpl never.
Set Warnings "-undo-batch-mode,-non-interactive".
Set Default Proof Using "Type".
From Undecidability Require Import TM.Code.Copy.
Definition CopyValue_sizefun {sigX X : Type} {cX : codable sigX X} (x : X) : Vector.t (nat->nat) 2 := [|id; CopyValue_size x|].
Lemma CopyValue_SpecT_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X)
(ss : Vector.t nat 2) :
TripleT (≃≃([],withSpace [|Contains _ x; Void|] ss))
(CopyValue_steps x) (CopyValue sig)
(fun _ => ≃≃([],withSpace ([|Contains _ x; Contains _ x|]) (appSize (CopyValue_sizefun x) ss))).
Proof.
start_TM.
eapply Realise_TripleT.
- eapply CopyValue_Realise.
- eapply CopyValue_Terminates.
- intros tin [] tout H HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1. cbn in *.
cbn in *; simpl_vector in *; cbn in *.
modpon H. intros i; destruct_fin i; cbn in *; eauto.
- intros tin k HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1.
cbn in *; simpl_vector in *; cbn in *. eauto.
Qed.
Lemma CopyValue_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
TripleT (≃≃([],[|Contains _ x; Void|])) (CopyValue_steps x) (CopyValue sig) (fun _ => ≃≃([],[|Contains _ x; Contains _ x|])).
Proof. eapply TripleT_RemoveSpace. cbn. intros s. apply CopyValue_SpecT_size. Qed.
Lemma Reset_SpecT_space (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t nat 1) :
TripleT (≃≃([],withSpace ([|Contains _ x|]) ss)) (Reset_steps x) (Reset sig) (fun _ => ≃≃([],withSpace ([|Void|]) (appSize [|Reset_size x|] ss))).
Proof.
start_TM.
eapply Realise_TripleT.
- eapply Reset_Realise.
- eapply Reset_Terminates.
- intros tin [] tout H HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0); cbn in *. simpl_vector in *; cbn in *.
modpon H. intros i; destruct_fin i; cbn; eauto.
- intros tin k HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. eauto.
Qed.
Lemma Reset_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
TripleT (≃≃([],[|Contains _ x|])) (Reset_steps x) (Reset sig) (fun _ => ≃≃([], [|Void|])).
Proof. eapply TripleT_RemoveSpace. apply Reset_SpecT_space. Qed.
Lemma Reset_Spec (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
Triple (≃≃([], [|Contains _ x|])) (Reset sig) (fun _ => ≃≃([], [|Void|])).
Proof. eapply TripleT_Triple. apply Reset_SpecT. Qed.
Definition MoveValue_size {X Y sigX sigY : Type} {cX : codable sigX X} {cY : codable sigY Y} (x : X) (y : Y) : Vector.t (nat->nat) 2 :=
[|MoveValue_size_x x; MoveValue_size_y x y|].
Lemma MoveValue_SpecT_size (sig : finType) (sigX sigY X Y : Type)
(cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) (ss : Vector.t nat 2) :
TripleT (≃≃([], withSpace ( [|Contains _ x; Contains _ y|]) ss)) (MoveValue_steps x y) (MoveValue sig)
(fun _ => ≃≃([], withSpace ( [|Void; Contains _ x|]) (appSize (MoveValue_size x y) ss))).
Proof.
start_TM.
eapply Realise_TripleT.
- apply MoveValue_Realise with (X := X) (Y := Y).
- apply MoveValue_Terminates with (X := X) (Y := Y).
- intros tin [] tout H HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1. simpl_vector in *; cbn in *.
modpon H. intros i; destruct_fin i; cbn; eauto.
- intros tin k HEnc. unfold withSpace in HEnc. cbn in *.
specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1. simpl_vector in *; cbn in *. eauto.
Qed.
Lemma MoveValue_SpecT (sig : finType) (sigX sigY X Y : Type)
(cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) :
TripleT (≃≃([], [|Contains _ x; Contains _ y|])) (MoveValue_steps x y) (MoveValue sig) (fun _ => ≃≃([], [|Void; Contains _ x|])).
Proof. eapply TripleT_RemoveSpace. apply MoveValue_SpecT_size. Qed.
Lemma MoveValue_Spec (sig : finType) (sigX sigY X Y : Type)
(cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) :
Triple (≃≃([], [|Contains _ x; Contains _ y|])) (MoveValue sig) (fun _ => ≃≃([], [|Void; Contains _ x|])).
Proof. eapply TripleT_Triple. apply MoveValue_SpecT. Qed.
Lemma Constr_O_SpecT_pure :
TripleT (fun tin => isVoid tin[@Fin0]) (Constr_O_steps) (Constr_O) (fun _ tout => tout[@Fin0] ≃ 0).
Proof.
start_TM.
eapply RealiseIn_TripleT.
- apply Constr_O_Sem.
- intros tin [] tout H1 H2. cbn in *. unfold tspec in *. modpon H1. unfold_abbrev. contains_ext.
Qed.
Lemma Constr_O_Spec_pure :
Triple (fun tin => isVoid tin[@Fin0]) (Constr_O) (fun _ tout => tout[@Fin0] ≃ 0).
Proof. eapply TripleT_Triple. apply Constr_O_SpecT_pure. Qed.
Lemma Constr_S_SpecT_pure (y : nat) :
TripleT (fun tin => tin[@Fin0] ≃ y) (Constr_S_steps) (Constr_S) (fun _ tout => tout[@Fin0] ≃ S y).
Proof.
eapply RealiseIn_TripleT.
- apply Constr_S_Sem.
- intros tin [] tout H1 H2. cbn in *. unfold tspec in *. modpon H1. contains_ext.
Qed.
Lemma Constr_S_Spec_pure (y : nat) :
Triple (fun tin => tin[@Fin0] ≃ y) (Constr_S) (fun _ tout => tout[@Fin0] ≃ (S y)).
Proof. eapply TripleT_Triple. apply Constr_S_SpecT_pure. Qed.
Lemma Constr_O_SpecT_size (ss : Vector.t nat 1) :
TripleT (≃≃([], withSpace ( [|Void|]) ss)) Constr_O_steps Constr_O (fun _ => ≃≃([], withSpace ( [|Contains _ 0|]) (appSize [|Constr_O_size|] ss))).
Proof.
start_TM.
eapply RealiseIn_TripleT.
- apply Constr_O_Sem.
- intros tin [] tout H1 H2. unfold withSpace in H2. cbn in *. unfold tspec in *. specialize (H2 Fin0). simpl_vector in *; cbn in *. modpon H1.
hnf. intros i; destruct_fin i; cbn; eauto.
Qed.
Lemma Constr_O_SpecT :
TripleT (≃≃([], [|Void|])) Constr_O_steps Constr_O (fun _ => ≃≃([], [|Contains _ 0|])).
Proof. eapply TripleT_RemoveSpace; apply Constr_O_SpecT_size. Qed.
Lemma Constr_O_Spec :
Triple (≃≃([], [|Void|])) Constr_O (fun _ => ≃≃([], [|Contains _ 0|])).
Proof. eapply TripleT_Triple. apply Constr_O_SpecT. Qed.
Lemma Constr_S_SpecT_size :
forall (y : nat) ss,
TripleT (≃≃([], withSpace ( [|Contains _ y|]) ss)) Constr_S_steps Constr_S
(fun _ => ≃≃([], withSpace ( [|Contains _ (S y)|]) (appSize [|S|] ss))).
Proof.
intros y ss. start_TM.
eapply RealiseIn_TripleT.
- apply Constr_S_Sem.
- intros tin [] tout H HEnc. unfold withSpace in *|-. cbn in *.
specialize (HEnc Fin0). simpl_vector in *; cbn in *. modpon H.
hnf. intros i; destruct_fin i; cbn; eauto.
Qed.
Lemma Constr_S_SpecT :
forall (y : nat), TripleT (≃≃([], [|Contains _ y|])) Constr_S_steps Constr_S (fun _ => ≃≃([], [|Contains _ (S y)|])).
Proof. intros. eapply TripleT_RemoveSpace; apply Constr_S_SpecT_size. Qed.
Lemma Constr_S_Spec :
forall (y : nat), Triple (≃≃([], [|Contains _ y|])) Constr_S (fun _ => ≃≃([], [|Contains _ (S y)|])).
Proof. intros y. eapply TripleT_Triple. apply Constr_S_SpecT. Qed.
Definition CaseNat_size (n : nat) : Vector.t (nat->nat) 1 :=
match n with
| O => [|id|]
| S n' => [|S|]
end.
Lemma CaseNat_SpecT_size (y : nat) (ss : Vector.t nat 1) :
TripleT
(≃≃([], withSpace ( [|Contains _ y|]) ss))
CaseNat_steps
CaseNat
(fun yout =>
tspec ([if yout then y <> 0 else y = 0],
(withSpace [|Contains _ (pred y)|] (appSize (CaseNat_size y) ss)))).
Proof.
start_TM.
eapply RealiseIn_TripleT.
- apply CaseNat_Sem.
- intros tin yout tout H HEnc. unfold withSpace in *|-. specialize (HEnc Fin0). simpl_vector in *; cbn in *. modpon H.
destruct yout, y; cbn in *; auto.
+ hnf. split. easy. intros i; destruct_fin i; cbn; eauto.
+ hnf. split. easy. intros i; destruct_fin i; cbn; eauto.
Qed.
Lemma CaseNat_SpecT (y : nat) :
TripleT
(≃≃([], [|Contains _ y|]))
CaseNat_steps
CaseNat
(fun yout =>
tspec ([if yout then y <> 0 else y = 0],[|Contains _ (pred y)|])).
Proof. eapply TripleT_RemoveSpace. apply CaseNat_SpecT_size. Qed.
Lemma CaseNat_Spec (y : nat) :
Triple (≃≃([], [|Contains _ y|]))
CaseNat
(fun yout =>
tspec
([if yout then y <> 0 else y = 0],[|Contains _ (pred y)|])).
Proof. eapply TripleT_Triple. apply CaseNat_SpecT. Qed.
Lemma Constr_S_Spec_con (n : nat) (Q : Assert sigNat^+ 1) :
(forall tout, ≃≃([], [|Contains _ (S n)|]) tout -> Q tout) ->
Triple (≃≃([], [|Contains _ n|])) Constr_S (fun _ => Q).
Proof. eauto using Consequence_post, Constr_S_Spec. Qed.
Ltac hstep_Nat :=
lazymatch goal with
| [ |- TripleT ?P ?k Constr_O ?Q ] => eapply Constr_O_SpecT_size
| [ |- TripleT ?P ?k Constr_S ?Q ] => eapply Constr_S_SpecT_size
| [ |- TripleT ?P ?k CaseNat ?Q ] => eapply CaseNat_SpecT_size
end.
Smpl Add hstep_Nat : hstep_Spec.
Definition IncrementTwice_steps := 1 + Constr_S_steps + Constr_S_steps.
Definition IncrementTwice : pTM sigNat^+ unit 1 := Constr_S;; Constr_S.
Lemma IncrementTwice_Spec_pure (y : nat) :
Triple (fun tin => tin[@Fin0] ≃ y) (IncrementTwice) (fun _ tout => tout[@Fin0] ≃ S (S y)).
Proof.
start_TM.
eapply Seq_Spec.
- apply Constr_S_Spec_pure.
- cbn. intros _. apply Constr_S_Spec_pure.
Restart.
start_TM.
unfold IncrementTwice. hsteps. apply Constr_S_Spec_pure.
cbn. intros _. apply Constr_S_Spec_pure.
Qed.
Lemma IncrementTwice_SpecT_pure (y : nat) :
TripleT (fun tin => tin[@Fin0] ≃ y) (IncrementTwice_steps) (IncrementTwice) (fun _ tout => tout[@Fin0] ≃ S (S y)).
Proof.
start_TM.
eapply Seq_SpecT.
- apply Constr_S_SpecT_pure.
- cbn. intros _. apply Constr_S_SpecT_pure.
- reflexivity. Restart.
start_TM.
unfold IncrementTwice. hsteps. apply Constr_S_SpecT_pure.
cbn. intros _. apply Constr_S_SpecT_pure.
reflexivity.
Qed.
Lemma IncrementTwice_Spec (y : nat) :
Triple (≃≃([], [|Contains _ y|])) (IncrementTwice) (fun _ => ≃≃([], [|Contains _ (S (S y))|])).
Proof.
start_TM.
eapply Seq_Spec.
- apply Constr_S_Spec.
- cbn. intros _. apply Constr_S_Spec.
Restart. start_TM.
unfold IncrementTwice. hstep. apply Constr_S_Spec.
cbn. intros _.
apply Constr_S_Spec. Restart.
start_TM.
unfold IncrementTwice.
hsteps_cbn. eauto.
Qed.
Lemma IncrementTwice_SpecT (y : nat) :
TripleT (≃≃([], [|Contains _ y|])) (IncrementTwice_steps) (IncrementTwice) (fun _ => ≃≃([], [|Contains _ (S (S y))|])).
Proof.
start_TM.
eapply Seq_SpecT.
- apply Constr_S_SpecT.
- cbn. intros _. apply Constr_S_SpecT.
- reflexivity.
Restart.
start_TM.
unfold IncrementTwice. hstep. apply Constr_S_SpecT.
cbn. intros _. apply Constr_S_SpecT. Restart. unfold IncrementTwice. hsteps_cbn.
eauto. reflexivity. Qed.
Definition Incr2 : pTM sigNat^+ unit 2 :=
Constr_S@[|Fin0|];; Constr_S@[|Fin1|].
Definition Incr2_steps := 1 + Constr_S_steps + Constr_S_steps.
Lemma Incr2_Spec :
forall (x y : nat), Triple (≃≃([], [|Contains _ x; Contains _ y|])) Incr2 (fun _ => ≃≃([], [|Contains _ (S x); Contains _ (S y)|])).
Proof.
intros x y. start_TM.
eapply Seq_Spec.
- eapply LiftTapes_Spec.
+ smpl_dupfree.
+ cbn. apply Constr_S_Spec.
- cbn. intros _. eapply LiftTapes_Spec_con. + smpl_dupfree.
+ cbn. apply Constr_S_Spec.
+ cbn. auto.
Restart.
intros x y. unfold Incr2.
hsteps_cbn. eauto.
Qed.
Lemma Incr2_SpecT :
forall (x y : nat), TripleT (≃≃([], [|Contains _ x; Contains _ y|])) Incr2_steps Incr2 (fun _ => ≃≃([], [|Contains _ (S x); Contains _ (S y)|])).
Proof.
intros x y. start_TM.
eapply Seq_SpecT.
- eapply LiftTapes_SpecT.
+ smpl_dupfree.
+ cbn. apply Constr_S_SpecT.
- intros []. cbn [Frame]. eapply LiftTapes_SpecT_con.
+ smpl_dupfree.
+ cbn. apply Constr_S_SpecT.
+ cbn. auto.
- reflexivity. Restart.
intros x y. unfold Incr2. hsteps_cbn. all:reflexivity.
Qed.
Definition Incr3 : pTM sigNat^+ unit 3 :=
Constr_S@[|Fin0|];; Constr_S@[|Fin1|];; IncrementTwice@[|Fin2|].
Definition Incr3_steps := 2 + Constr_S_steps + Constr_S_steps + IncrementTwice_steps.
Lemma Incr3_Spec :
forall (x y z : nat), Triple (≃≃([], [|Contains _ x; Contains _ y; Contains _ z|])) Incr3 (fun _ => ≃≃([], [|Contains _ (S x); Contains _ (S y); Contains _ (S (S z))|])).
Proof.
intros x y z. start_TM.
eapply Seq_Spec.
- eapply LiftTapes_Spec.
+ smpl_dupfree.
+ cbn. apply Constr_S_Spec.
- intros []. cbn [Frame].
eapply Seq_Spec. + eapply LiftTapes_Spec.
* smpl_dupfree.
* cbn. apply Constr_S_Spec.
+ intros []. cbn [Frame].
eapply LiftTapes_Spec_con. * smpl_dupfree.
* cbn. apply IncrementTwice_Spec.
* cbn. auto. Restart.
intros x y z. unfold Incr3.
hsteps_cbn. apply IncrementTwice_Spec. cbn. eauto.
Qed.
Lemma Incr3_SpecT :
forall (x y z : nat), TripleT (≃≃([], [|Contains _ x; Contains _ y; Contains _ z|])) (Incr3_steps) Incr3 (fun _ => ≃≃([], [|Contains _ (S x); Contains _ (S y); Contains _ (S (S z))|])).
Proof.
intros x y z. start_TM.
eapply Seq_SpecT.
- eapply LiftTapes_SpecT.
+ smpl_dupfree.
+ cbn. apply Constr_S_SpecT.
- intros []. cbn [Frame].
eapply Seq_SpecT.
+ eapply LiftTapes_SpecT.
* smpl_dupfree.
* cbn. apply Constr_S_SpecT.
+ intros []. cbn [Frame].
eapply LiftTapes_SpecT_con.
* smpl_dupfree.
* cbn. apply IncrementTwice_SpecT.
* cbn. auto.
+ reflexivity. - reflexivity. Restart.
intros x y z. unfold Incr3.
hsteps_cbn. apply IncrementTwice_SpecT. cbn. eauto. reflexivity. reflexivity.
Qed.
Definition Add_Step : pTM sigNat^+ (option unit) 2 :=
If (CaseNat @ [|Fin1|])
(Return (Constr_S @ [|Fin0|]) None)
(Return Nop (Some tt)).
Definition Add_Step_Post : nat*nat -> option unit -> Assert sigNat^+ 2 :=
fun '(a,b) =>
(fun yout =>
≃≃(([yout = if b then Some tt else None]
,[|Contains _ (match b with 0 => a | _ => S a end);Contains _ (pred b)|]))).
Lemma Add_Step_Spec (a b : nat) :
Triple (≃≃([], [|Contains _ a; Contains _ b|])) Add_Step
(Add_Step_Post (a,b)).
Proof.
start_TM.
eapply If_Spec.
- apply LiftTapes_Spec.
+ smpl_dupfree.
+ cbn. eapply CaseNat_Spec.
- cbn. hintros ?. destruct b as [ | b']; cbn [Frame]. contradiction.
eapply Return_Spec_con.
+ cbn [Vector.nth Vector.caseS Vector.case0].
apply LiftTapes_Spec.
* smpl_dupfree.
* cbn [Downlift select]. apply Constr_S_Spec.
+ cbn. intros. tspec_ext.
- cbn. hintros ->.
eapply Return_Spec_con.
+ cbn [Vector.nth Vector.caseS Vector.case0]. apply Nop_Spec.
+ intros []. tspec_ext.
Qed.
Definition Add_Loop : pTM sigNat^+ unit 2 := While Add_Step.
Lemma Add_Loop_Spec (a b : nat) :
Triple (≃≃([], [|Contains _ a; Contains _ b|]))
Add_Loop
(fun _ => ≃≃([], [|Contains _ (a+b); Contains _ 0|])).
Proof.
eapply While_SpecReg with
(P := fun '(a,b) => (_,_))
(Q := fun '(a,b) y => (_,_))
(R := fun '(a,b) y => (_,_)) (x := (a,b)).
- intros (x,y). eapply Add_Step_Spec. - intros (x,y);cbn. split.
+intros []. destruct y; intros [=].
replace (x+0) with x by lia. auto.
+destruct y;intros [=]. eexists (_,_). split.
*tspec_ext.
*cbn. tspec_ext. f_equal. nia.
Qed.
Definition Add_Step_steps : nat := 9.
Lemma Add_Step_SpecT (a b : nat) :
TripleT (≃≃([], [|Contains _ a; Contains _ b|]))
Add_Step_steps
Add_Step
(Add_Step_Post (a,b)).
Proof.
start_TM.
unfold Add_Step. eapply If_SpecT with (k3 := 0). hsteps. all:cbn beta.
- destruct b as [ | b']; cbn in *; auto. all:hintros ?. contradiction.
hsteps. cbn. tspec_ext.
- destruct b as [ | b']; cbn in *; auto. all:hintros ?. 2:congruence.
hsteps. cbn. tspec_ext.
-cbn. intros. destruct yout. reflexivity. unfold CaseNat_steps, Add_Step_steps. lia.
Qed.
Definition Add_Step_size (a b : nat) : Vector.t (nat->nat) 2 :=
match b with
| 0 => [|id; id|]
| S b' => [|S; S|]
end.
Lemma Add_Step_SpecT_space (a b : nat) (ss : Vector.t nat 2) :
TripleT
(≃≃([], withSpace ( [|Contains _ a; Contains _ b|]) ss))
Add_Step_steps
Add_Step
(fun yout =>
≃≃([yout = if b then Some tt else None]
,withSpace [|Contains _ (match b with 0 => a | _ => S a end);Contains _ (pred b)|]
(appSize (Add_Step_size a b) ss))).
Proof.
start_TM.
unfold Add_Step. eapply If_SpecT with (k3 := 0).
- hsteps_cbn.
- cbn. hintros ?. destruct b as [ | b']; cbn in *. easy. hsteps_cbn; cbn. tspec_ext.
- cbn. hintros ->. hsteps. cbn. tspec_ext.
- intros. destruct yout. + reflexivity.
+ unfold CaseNat_steps, Add_Step_steps. lia.
Qed.
Definition Add_Loop_steps b := 9 + 10 * b.
Lemma Add_Loop_SpecT (a b : nat) :
TripleT (≃≃([], [|Contains _ a; Contains _ b|]))
(Add_Loop_steps b)
(Add_Loop)
(fun _ => ≃≃([], [|Contains _ (a+b); Contains _ 0|])).
Proof.
unfold Add_Loop. eapply While_SpecTReg with
(PRE := fun '(a,b) => (_,_)) (INV := fun '(a,b) y => (_,_)) (POST := fun '(a,b) y => (_,_))
(f__step := fun '(a,b) => _) (f__loop := fun '(a,b) => _) (x := (a,b)).
- intros (x,y). eapply Add_Step_SpecT. - intros (x,y);cbn. split.
+ intros []. split.
* destruct y as [ | y'];cbn. 2:intros;congruence. tspec_ext. f_equal. nia.
*unfold Add_Step_steps,Add_Loop_steps. nia.
+destruct y as [ | y']; cbn in *; auto. easy. intros _.
eexists (S x, y') ; cbn. repeat split.
* tspec_ext.
* unfold Add_Step_steps, Add_Loop_steps. lia.
* tspec_ext. f_equal. nia.
Qed.
Fixpoint Add_Loop_size (a b : nat) : Vector.t (nat->nat) 2 :=
match b with
| O => Add_Step_size a b
| S b' => Add_Step_size a b >>> Add_Loop_size (S a) b'
end.
Lemma Add_Loop_SpecT_size (a b : nat) (ss : Vector.t nat 2) :
TripleT
(≃≃([], withSpace ( [|Contains _ a; Contains _ b|]) ss))
(Add_Loop_steps b)
(Add_Loop)
(fun _ => tspec
([], withSpace [|Contains _ (a+b); Contains _ 0|]
(appSize (Add_Loop_size a b) ss))).
Proof.
eapply While_SpecTReg with (PRE := fun '(a,b,ss) => (_,_)) (INV := fun '(a,b,ss) y => (_,_))
(POST := fun '(a,b,ss) y => (_,_)) (f__loop := fun '(a,b,ss) => _) (f__step := fun '(a,b,ss) => _) (x := (a,b,ss));
clear a b ss; intros ((x,y),ss).
- apply Add_Step_SpecT_space.
- cbn. split.
+intros []. split. 2:unfold Add_Step_steps, Add_Loop_steps;lia.
destruct y as [ | y']; cbn in *. 2:easy. tspec_ext. f_equal. nia.
+destruct y as [ | y']; cbn in *. easy. intros _.
eexists (S x, y', _); cbn. repeat split.
* tspec_ext.
* unfold Add_Step_steps, Add_Loop_steps. lia.
* tspec_ext. f_equal. nia.
Qed.
Definition Add : pTM sigNat^+ unit 4 :=
LiftTapes (CopyValue _) [|Fin1; Fin2|];;
LiftTapes (CopyValue _) [|Fin0; Fin3|];;
LiftTapes Add_Loop [|Fin2; Fin3|];;
LiftTapes (Reset _) [|Fin3|].
Definition Add_steps m n := 98 + 12 * n + 22 * m.
Lemma Add_SpecT (a b : nat) :
TripleT (≃≃([], [|Contains _ a; Contains _ b; Void; Void|]))
(Add_steps a b)
Add
(fun _ => ≃≃([], [|Contains _ a; Contains _ b; Contains _ (a+b); Void|])).
Proof.
start_TM.
eapply Seq_SpecT.
eapply LiftTapes_SpecT. smpl_dupfree. eapply CopyValue_SpecT.
intros []. cbn.
eapply Seq_SpecT.
eapply LiftTapes_SpecT. smpl_dupfree. eapply CopyValue_SpecT.
intros []. cbn.
eapply Seq_SpecT.
apply LiftTapes_SpecT. smpl_dupfree. cbn. apply Add_Loop_SpecT.
cbn. intros _.
eapply LiftTapes_SpecT_con. smpl_dupfree. eapply Reset_SpecT.
cbn. intros _. tspec_ext. f_equal. nia.
reflexivity. reflexivity.
unfold CopyValue_steps, Add_Loop_steps, Add_steps, Reset_steps. rewrite !Encode_nat_hasSize. lia.
Restart.
start_TM.
unfold Add. hsteps_cbn. now apply Add_Loop_SpecT. now apply Reset_SpecT.
replace (a+b) with (b+a) by lia. auto.
reflexivity. reflexivity.
unfold CopyValue_steps, Add_Loop_steps, Add_steps, Reset_steps. rewrite !Encode_nat_hasSize. lia.
Qed.
Definition Add_space (a b : nat) : Vector.t (nat->nat) 4 :=
[| id; id; CopyValue_size b >> Add_Loop_size b a @>Fin0;
CopyValue_size a >> (Add_Loop_size b a @>Fin1) >> Reset_size 0 |].
Lemma Add_SpecT_space (a b : nat) (ss : Vector.t nat 4) :
TripleT
(≃≃([], withSpace ( [|Contains _ a; Contains _ b; Void; Void|]) ss))
(Add_steps a b)
Add
(fun _ => ≃≃([], withSpace ( [|Contains _ a; Contains _ b; Contains _ (a+b); Void|])
(appSize (Add_space a b) ss))).
Proof. start_TM.
unfold Add.
hstep. hstep.
apply CopyValue_SpecT_size.
cbn. intros _. cbn.
hstep. cbn. hstep. cbn. apply CopyValue_SpecT_size.
cbn. intros _. hstep. cbn. hstep. cbn. apply Add_Loop_SpecT_size.
cbn. intros _. hstep. cbn. apply Reset_SpecT_space.
cbn. intros _. replace (b+a) with (a+b) by lia. auto.
reflexivity. reflexivity.
unfold CopyValue_steps, Reset_steps, Add_Loop_steps, Add_steps. rewrite !Encode_nat_hasSize. lia.
Qed.
Definition Mult_Step : pTM sigNat^+ (option unit) 5 :=
If (LiftTapes CaseNat [|Fin0|])
(Return (
LiftTapes Add [|Fin1; Fin2; Fin3; Fin4|];;
LiftTapes (MoveValue _) [|Fin3; Fin2|]
) (None))
(Return Nop (Some tt)).
Definition Mult_Step_Post : nat*nat*nat -> option unit -> Assert sigNat^+ 5 :=
fun '(m',n,c) =>
(fun yout =>
≃≃([yout = if m' then Some tt else None],
[|Contains _ (pred m'); Contains _ n; Contains _ ( if m' then c else (n + c)); Void; Void|])).
Definition Mult_Step_steps m' n c :=
match m' with
| O => 6
| _ => 168 + 33 * c + 39 * n
end.
Lemma Mult_Step_SpecT m' n c :
TripleT
(≃≃([], [|Contains _ m'; Contains _ n; Contains _ c; Void; Void|]))
(Mult_Step_steps m' n c)
(Mult_Step)
((Mult_Step_Post) (m',n,c)).
Proof.
start_TM.
eapply If_SpecTReg.
- apply LiftTapes_SpecT. smpl_dupfree. cbn. apply CaseNat_SpecT.
- cbn. destruct m' as [ | m'']; cbn; auto. all:hintros ?. easy.
eapply Return_SpecT_con.
+ eapply Seq_SpecT.
eapply LiftTapes_SpecT. smpl_dupfree. cbn. apply Add_SpecT.
cbn. intros []. apply LiftTapes_SpecT. smpl_dupfree. cbn. apply MoveValue_SpecT.
reflexivity.
+ cbn. tspec_ext.
- cbn. destruct m' as [ | m'']; cbn; auto. all:hintros ?. 2:easy.
eapply Return_SpecT_con.
apply Nop_SpecT. cbn. tspec_ext.
- cbn. intros b.
unfold Mult_Step_steps, MoveValue_steps, CaseNat_steps, Add_steps.
destruct b,m';intros H ;rewrite ?Encode_nat_hasSize. all:nia.
Restart.
eapply If_SpecTReg.
- hsteps.
- cbn. hintros Hm.
hsteps. apply Add_SpecT. cbn. hsteps. reflexivity. cbn.
destruct m'. easy. cbn. tspec_ext.
- cbn. hsteps. hintros ? ->. tspec_ext.
- cbn. intros b. unfold Mult_Step_steps, MoveValue_steps, CaseNat_steps, Add_steps.
destruct b,m';intros H ;rewrite ?Encode_nat_hasSize. all:nia.
Qed.
Definition Mult_Step_space m' n c : Vector.t (nat->nat) 5 :=
match m' with
| 0 => [|id; id; id; id; id|]
| S m'' => [| S;
Add_space n c @> Fin0;
(Add_space n c @> Fin1) >> MoveValue_size_y (n+c) c;
(Add_space n c @> Fin2) >> MoveValue_size_x (n+c);
(Add_space n c @>Fin3) |]
end.
Lemma Mult_Step_SpecT_size m' n c ss :
TripleT
(≃≃([], withSpace ( [|Contains _ m'; Contains _ n; Contains _ c; Void; Void|]) ss))
(Mult_Step_steps m' n c)
(Mult_Step)
(fun yout =>
≃≃([yout = if m' then Some tt else None],
withSpace
[|Contains _ (pred m'); Contains _ n; Contains _ ( if m' then c else (n + c)); Void; Void|] (appSize (Mult_Step_space m' n c) ss))).
Proof.
start_TM.
eapply If_SpecTReg.
- hsteps.
- cbn. hintros ?. destruct m' as [ | m'']. contradiction. cbn.
hsteps. apply Add_SpecT_space. cbn. hsteps. cbn. reflexivity. cbn. tspec_ext.
- cbn. hintros ->. hsteps. tspec_ext.
- cbn. destruct m'; intros []. 1,4:easy.
all:unfold Mult_Step_steps, MoveValue_steps, CaseNat_steps, Add_steps. 2:rewrite !Encode_nat_hasSize.
all:lia.
Qed.
Definition Mult_Loop := While Mult_Step.
Fixpoint Mult_Loop_steps m' n c :=
match m' with
| O => S (Mult_Step_steps m' n c)
| S m'' => S (Mult_Step_steps m' n c) + Mult_Loop_steps m'' n (n + c)
end.
Lemma Mult_Loop_SpecT m' n c :
TripleT
(≃≃([], [|Contains _ m'; Contains _ n; Contains _ c; Void; Void|]))
(Mult_Loop_steps m' n c)
(Mult_Loop)
(fun _ => ≃≃([], [|Contains _ 0; Contains _ n; Contains _ (m' * n + c); Void; Void|])).
Proof.
unfold Mult_Loop.
eapply While_SpecTReg with (PRE := fun '(m',n,c) => (_,_)) (INV := fun '(m',n,c) y => (_,_)) (POST := fun '(m',n,c) y => (_,_))
(f__loop := fun '(m,n,c) => _) (f__step := fun '(m,n,c) => _) (x:=(m',n,c)) ; clear m' n c;intros ((m'&n')&c).
- apply Mult_Step_SpecT.
- cbn. split.
+ intros y H. destruct m'. 2:easy. split. 2:{ cbn. nia. } tspec_ext.
+ destruct m'. easy. cbn. eexists (_,_,_). split. tspec_ext. split. nia. tspec_ext. f_equal. nia.
Qed.
Fixpoint Mult_Loop_size m' n c :=
match m' with
| 0 => Mult_Step_space m' n c
| S m'' => Mult_Step_space m' n c >>> Mult_Loop_size m'' n (n+c)
end.
Lemma Mult_Loop_SpecT_size m' n c ss :
TripleT
(≃≃([], withSpace ( [|Contains _ m'; Contains _ n; Contains _ c; Void; Void|]) ss))
(Mult_Loop_steps m' n c)
(Mult_Loop)
(fun _ => ≃≃([],withSpace
[|Contains _ 0; Contains _ n; Contains _ (m' * n + c); Void; Void|]
(appSize (Mult_Loop_size m' n c) ss))).
Proof.
eapply While_SpecTReg with (PRE := fun '(m',n,c,ss) => (_,_)) (INV := fun '(m',n,c,ss) y => (_,_)) (POST := fun '(m',n,c,ss) y => (_,_))
(f__loop := fun '(m,n,c,ss) => _) (f__step := fun '(m,n,c,ss) => _) (x := (m',n,c,ss));
clear m' n c ss; intros (((m',n),c),ss).
- apply Mult_Step_SpecT_size.
- cbn. split.
+intros y Hy. destruct m'. 2:easy. split. 2:cbn;lia. tspec_ext.
+destruct m'. easy. intros _. eexists (_,_,_,_). repeat split.
*tspec_ext.
*cbn;nia.
*tspec_ext. f_equal. cbn. nia.
Qed.
Definition Mult : pTM sigNat^+ unit 6 :=
LiftTapes (CopyValue _) [|Fin0; Fin5|];;
LiftTapes (Constr_O) [|Fin2|];;
LiftTapes Mult_Loop [|Fin5; Fin1; Fin2; Fin3; Fin4|];;
LiftTapes (Reset _) [|Fin5|].
Definition Mult_steps (m n : nat) : nat := 12 * m + Mult_Loop_steps m n 0 + 57.
Lemma Mult_SpecT (m n : nat) :
TripleT
(≃≃([], [|Contains _ m; Contains _ n; Void; Void; Void; Void|]))
(Mult_steps m n)
(Mult)
(fun _ => ≃≃([], [|Contains _ m; Contains _ n; Contains _ (m * n); Void; Void; Void|])).
Proof.
start_TM.
eapply Seq_SpecT.
apply LiftTapes_SpecT. smpl_dupfree. apply CopyValue_SpecT.
cbn. intros _. eapply Seq_SpecT.
apply LiftTapes_SpecT. smpl_dupfree. apply Constr_O_SpecT.
cbn. intros _. eapply Seq_SpecT.
apply LiftTapes_SpecT. smpl_dupfree. apply Mult_Loop_SpecT.
cbn. intros _.
eapply LiftTapes_SpecT_con. smpl_dupfree. apply Reset_SpecT.
cbn. intros _. replace (m * n + 0) with (m * n) by lia. auto.
reflexivity. reflexivity.
unfold Mult_steps. ring_simplify. unfold CopyValue_steps, Constr_O_steps, Reset_steps. rewrite !Encode_nat_hasSize. cbn. ring_simplify. reflexivity.
Restart.
unfold Mult. hsteps_cbn.
apply Mult_Loop_SpecT. apply Reset_SpecT.
cbn. replace (m * n + 0) with (m * n) by lia. auto. reflexivity. reflexivity.
unfold Mult_steps. ring_simplify. unfold CopyValue_steps, Constr_O_steps, Reset_steps. rewrite !Encode_nat_hasSize. cbn. ring_simplify. reflexivity.
Qed.
Definition Mult_size_bug (m n : nat) : Vector.t (nat->nat) 6 :=
[| id;
Mult_Loop_size m n 0 @> Fin1;
Constr_O_size >> Mult_Loop_size m n 0 @> Fin2;
Mult_Loop_size m n 0 @> Fin3;
Mult_Loop_size m n 0 @> Fin4;
CopyValue_size m >> Mult_Loop_size m n 0 @> Fin4
|].
Lemma Mult_SpecT_space (m n : nat) (ss : Vector.t nat 6) :
TripleT
(≃≃([], withSpace ( [|Contains _ m; Contains _ n; Void; Void; Void; Void|]) ss))
(Mult_steps m n)
(Mult)
(fun _ => ≃≃([], withSpace ( [|Contains _ m; Contains _ n; Contains _ (m * n); Void; Void; Void|])
(appSize (Mult_size_bug m n) ss))).
Proof.
start_TM.
unfold Mult.
hstep. hstep. cbn.
apply CopyValue_SpecT_size.
cbn. intros _. hsteps.
cbn. intros _. hstep. cbn. hstep. cbn. apply Mult_Loop_SpecT_size.
cbn. intros. hstep. cbn. apply Reset_SpecT_space.
cbn. intros _. replace (m * n + 0) with (m * n) by lia.
Fail now auto. tspec_ext. Abort.
Definition Mult_size (m n : nat) : Vector.t (nat->nat) 6 :=
[| id;
Mult_Loop_size m n 0 @> Fin1;
Constr_O_size >> Mult_Loop_size m n 0 @> Fin2;
Mult_Loop_size m n 0 @> Fin3;
Mult_Loop_size m n 0 @> Fin4;
CopyValue_size m >> Mult_Loop_size m n 0 @> Fin0 >> Reset_size 0
|].
Lemma Mult_SpecT_space (m n : nat) (ss : Vector.t nat 6) :
TripleT
(≃≃([], withSpace ( [|Contains _ m; Contains _ n; Void; Void; Void; Void|]) ss))
(Mult_steps m n)
(Mult)
(fun _ => ≃≃([], withSpace ( [|Contains _ m; Contains _ n; Contains _ (m * n); Void; Void; Void|])
(appSize (Mult_size m n) ss))).
Proof.
start_TM.
unfold Mult.
hstep. hstep. cbn.
apply CopyValue_SpecT_size.
cbn. intros _. hsteps.
cbn. intros _. hstep. cbn. hstep. cbn. apply Mult_Loop_SpecT_size.
cbn. intros. hstep. cbn. apply Reset_SpecT_space.
cbn. intros t. replace (m * n + 0) with (m * n) by lia. auto.
reflexivity. reflexivity.
unfold Mult_steps. ring_simplify. unfold CopyValue_steps, Constr_O_steps, Reset_steps. rewrite !Encode_nat_hasSize. cbn. ring_simplify. reflexivity.
Qed.