From Undecidability.TM.Code Require Import ProgrammingTools.
From Undecidability Require Import TM.Code.CaseNat.
(* Minus x y computes x - y and returns whether x >= y (e.g., if the subtraction did not need to truncate) *)
Definition Subtract_Rel : pRel (sigNat^+) bool 2 :=
fun tin '(b, tout) =>
forall (x y : nat),
tin [@Fin0] ≃ x
-> tin [@Fin1] ≃ y
-> tout [@Fin0] ≃ x - y
/\ isVoid tout [@Fin1]
/\ b = (y <=? x).
Definition Subtract :pTM (sigNat^+) bool 2:=
While (
If(CaseNat @ [|Fin1|])
(If (CaseNat @ [|Fin0|])
(Return Nop None)
(Return (Reset _ @ [|Fin1|]) (Some false)) )
(Return (Reset _ @ [|Fin1|]) (Some true))
).
Lemma Subtract_Realise : Subtract ⊨ Subtract_Rel.
Proof.
eapply Realise_monotone.
{
unfold Subtract. TM_Correct. all: (try (notypeclasses refine (@Reset_Realise _ _ _ _ _);shelve)).
}
{
apply WhileInduction.
- intros tin b tout [(t0_&Hif1&[Hif2|[t1_ Hif2]]) |?] x y;TMSimp;[ | ].
+ modpon H. modpon H2. destruct y. easy. destruct x. 2:easy.
modpon H1. rewrite Nat.sub_0_l. cbn ["<=?"]. repeat split. contains_ext. isVoid_mono.
+ modpon H. destruct y. 2:easy.
modpon H1. rewrite Nat.sub_0_r. cbn ["<=?"]. repeat split. contains_ext. isVoid_mono.
- intros tin tmid tout b [(t0_&Hif1&[Hif2|[t1_ Hif2]]) |?] H' x y;TMSimp;[].
modpon H. modpon H1. destruct x,y;try contradiction;[].
modpon H'. rewrite Nat.sub_succ. cbn ["<=?"]. easy.
}
Qed.
From Undecidability Require Import UpToC Hoare.
Theorem Subtract_SpecT:
{ f : UpToC (fun x => x + 1) & forall (x y : nat),
TripleT ≃≃([],[|Contains _ x;Contains _ y|])
(f (y)) Subtract
(fun b => ≃≃([b = (y <=? x)],
([|Contains _ (x-y);Void|])))}.
Proof.
eexists_UpToC f. intros x y.
unfold Subtract.
eapply ConsequenceT.
refine (While_SpecTReg (PRE := fun '(x,y) => (_,_))
(INV := fun '(x,y) b => ([b = match y with 0 => Some true | _ => match x with 0 => Some false | _ => None end end]
,match y with 0 => [|Contains _ x;Void|] | S y' => [|Contains _ (pred x);match x with 0 => Void | _ => Contains _ y' end|] end))
(POST := fun '(x,y) b => (_,_)) (f__loop := fun '(x,y) => _)
(f__step := fun '(x,y) => match y with 0 => _ : nat | S y' => _ end ) _ _ ((x,y))); clear x y; intros (x,y).
3:{ cbn. reflexivity. }
3:{ cbn. reflexivity. }
3:{ cbn. reflexivity. }
-cbn. hstep.
+now hsteps_cbn.
+refine (_ : TripleT _ match y with 0 => _ | S _ => match x with 0 => _ | _ => _ end end _ _).
destruct y;hintros Hy. nia. hstep.
*now hsteps_cbn.
* cbn. destruct x;hintros ?. nia. hsteps_cbn. tspec_ext.
*cbn. hintros ->. cbn. hsteps_cbn. tspec_ext.
*cbn. intros b Hb. destruct b,x. 1,4:exfalso;nia. all:reflexivity.
+cbn. hintros ->. hsteps_cbn. tspec_ext.
+cbn - ["+" "*"]. intros b Hb.
destruct y,b. 1,4:exfalso;nia. all:reflexivity.
- cbn. split.
+ intros b Hb. destruct y.
{ inv Hb. cbn - ["+"]. rewrite Nat.sub_0_r. split. now tspec_ext. shelve. }
split. 2:shelve.
destruct x. all:inv Hb. cbn. tspec_ext.
+ destruct y. easy. destruct x. easy.
eexists (_,_). split. cbn. reflexivity.
split. shelve. cbn. reflexivity.
- Unshelve.
4,5,6:unfold Reset_steps;rewrite ?Encode_nat_hasSize;ring_simplify.
[f]:exact (fun y => y * 30 + CaseNat_steps + 30).
2:exact 0.
1:now subst f;smpl_upToC_solve.
all:unfold f.
2:destruct x.
all:nia.
Qed.
Ltac hstep_Subtract :=
lazymatch goal with
| [ |- TripleT ?P ?k Subtract ?Q ] => notypeclasses refine (projT2 Subtract_SpecT _ _);shelve
end.
Smpl Add hstep_Subtract : hstep_Spec.
From Undecidability Require Import TM.Code.CaseNat.
(* Minus x y computes x - y and returns whether x >= y (e.g., if the subtraction did not need to truncate) *)
Definition Subtract_Rel : pRel (sigNat^+) bool 2 :=
fun tin '(b, tout) =>
forall (x y : nat),
tin [@Fin0] ≃ x
-> tin [@Fin1] ≃ y
-> tout [@Fin0] ≃ x - y
/\ isVoid tout [@Fin1]
/\ b = (y <=? x).
Definition Subtract :pTM (sigNat^+) bool 2:=
While (
If(CaseNat @ [|Fin1|])
(If (CaseNat @ [|Fin0|])
(Return Nop None)
(Return (Reset _ @ [|Fin1|]) (Some false)) )
(Return (Reset _ @ [|Fin1|]) (Some true))
).
Lemma Subtract_Realise : Subtract ⊨ Subtract_Rel.
Proof.
eapply Realise_monotone.
{
unfold Subtract. TM_Correct. all: (try (notypeclasses refine (@Reset_Realise _ _ _ _ _);shelve)).
}
{
apply WhileInduction.
- intros tin b tout [(t0_&Hif1&[Hif2|[t1_ Hif2]]) |?] x y;TMSimp;[ | ].
+ modpon H. modpon H2. destruct y. easy. destruct x. 2:easy.
modpon H1. rewrite Nat.sub_0_l. cbn ["<=?"]. repeat split. contains_ext. isVoid_mono.
+ modpon H. destruct y. 2:easy.
modpon H1. rewrite Nat.sub_0_r. cbn ["<=?"]. repeat split. contains_ext. isVoid_mono.
- intros tin tmid tout b [(t0_&Hif1&[Hif2|[t1_ Hif2]]) |?] H' x y;TMSimp;[].
modpon H. modpon H1. destruct x,y;try contradiction;[].
modpon H'. rewrite Nat.sub_succ. cbn ["<=?"]. easy.
}
Qed.
From Undecidability Require Import UpToC Hoare.
Theorem Subtract_SpecT:
{ f : UpToC (fun x => x + 1) & forall (x y : nat),
TripleT ≃≃([],[|Contains _ x;Contains _ y|])
(f (y)) Subtract
(fun b => ≃≃([b = (y <=? x)],
([|Contains _ (x-y);Void|])))}.
Proof.
eexists_UpToC f. intros x y.
unfold Subtract.
eapply ConsequenceT.
refine (While_SpecTReg (PRE := fun '(x,y) => (_,_))
(INV := fun '(x,y) b => ([b = match y with 0 => Some true | _ => match x with 0 => Some false | _ => None end end]
,match y with 0 => [|Contains _ x;Void|] | S y' => [|Contains _ (pred x);match x with 0 => Void | _ => Contains _ y' end|] end))
(POST := fun '(x,y) b => (_,_)) (f__loop := fun '(x,y) => _)
(f__step := fun '(x,y) => match y with 0 => _ : nat | S y' => _ end ) _ _ ((x,y))); clear x y; intros (x,y).
3:{ cbn. reflexivity. }
3:{ cbn. reflexivity. }
3:{ cbn. reflexivity. }
-cbn. hstep.
+now hsteps_cbn.
+refine (_ : TripleT _ match y with 0 => _ | S _ => match x with 0 => _ | _ => _ end end _ _).
destruct y;hintros Hy. nia. hstep.
*now hsteps_cbn.
* cbn. destruct x;hintros ?. nia. hsteps_cbn. tspec_ext.
*cbn. hintros ->. cbn. hsteps_cbn. tspec_ext.
*cbn. intros b Hb. destruct b,x. 1,4:exfalso;nia. all:reflexivity.
+cbn. hintros ->. hsteps_cbn. tspec_ext.
+cbn - ["+" "*"]. intros b Hb.
destruct y,b. 1,4:exfalso;nia. all:reflexivity.
- cbn. split.
+ intros b Hb. destruct y.
{ inv Hb. cbn - ["+"]. rewrite Nat.sub_0_r. split. now tspec_ext. shelve. }
split. 2:shelve.
destruct x. all:inv Hb. cbn. tspec_ext.
+ destruct y. easy. destruct x. easy.
eexists (_,_). split. cbn. reflexivity.
split. shelve. cbn. reflexivity.
- Unshelve.
4,5,6:unfold Reset_steps;rewrite ?Encode_nat_hasSize;ring_simplify.
[f]:exact (fun y => y * 30 + CaseNat_steps + 30).
2:exact 0.
1:now subst f;smpl_upToC_solve.
all:unfold f.
2:destruct x.
all:nia.
Qed.
Ltac hstep_Subtract :=
lazymatch goal with
| [ |- TripleT ?P ?k Subtract ?Q ] => notypeclasses refine (projT2 Subtract_SpecT _ _);shelve
end.
Smpl Add hstep_Subtract : hstep_Spec.