Commit a65a59a8 authored by Ralf Jung's avatar Ralf Jung

make it possible to state contractiveness for any function (not just non-expansive ones).

This gets rid of an unnecessary proof obligation for wpF.
parent 0846921f
......@@ -50,8 +50,8 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
(forall HSafe : safe = true, safeExpr e σ).
(* Define the function wp will be a fixed-point of *)
Program Definition wpF safe m : (expr -n> vPred -n> Props) -n> (expr -n> vPred -n> Props) :=
n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])])].
Program Definition wpF safe m : (expr -n> vPred -n> Props) -> (expr -n> vPred -n> Props) :=
fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])].
Next Obligation.
intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
rewrite <- EQr, (comm rd), <- assoc in HE.
......@@ -165,26 +165,6 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
simpl in EQe; subst e2; reflexivity.
Qed.
Next Obligation.
intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
split; intros Hp w'; intros; edestruct Hp as [HF [HS [HV HS'] ] ]; try eassumption; [|].
- split; [assumption | split; [| split]; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
exists w'' r'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; omega.
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
exists w'' rfk rret; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+ auto.
- split; [assumption | split; [| split]; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
exists w'' r'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; omega.
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
exists w'' rfk rret; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+ auto.
Qed.
Instance contr_wpF safe m : contractive (wpF safe m).
Proof.
......
......@@ -305,7 +305,14 @@ Section MCont.
Context `{cT : cmetric T} `{cU : cmetric U} `{cV : cmetric V}.
(** Definition of contractive functions. This works since the spaces are bisected. *)
Class contractive (f : T -n> U) := contr n : Proper (dist n ==> dist (S n)) f.
Class contractive (f : T -> U) := contr n : Proper (dist n ==> dist (S n)) f.
Program Definition contractive_nonexp (f: T -> U) (fC: contractive f): T -n> U :=
n[(f)].
Next Obligation.
intros t u EQ. eapply dist_mono, fC. assumption.
Qed.
(** Image of a Cauchy chain by a non-expansive function is another Cauchy sequence. *)
Definition liftc (f : T -> U) (σ : chain T) : chain U := fun i => f (σ i).
......@@ -452,15 +459,20 @@ Section Fixpoints.
(** Stating that the proposed fixed point is in fact a fixed point. *)
Lemma fixp_eq f x {HC : contractive f} : fixp f x == f (fixp f x).
Proof.
pose (f' := contractive_nonexp _ HC).
change (fixp f' x == f' (fixp f' x)).
rewrite <- dist_refl; intros n; unfold fixp.
destruct (conv_cauchy (fun n => iter n f x) n) as [m Hm].
destruct (conv_cauchy (fun n => iter n f' x) n) as [m Hm].
rewrite (Hm (S (max n m))), (Hm (max n m)) at 1; simpl; reflexivity || apply _.
Qed.
Lemma fixp_iter f x i {HC : contractive f} : fixp f x == iter i f (fixp f x).
Proof.
pose (f' := contractive_nonexp _ HC).
change (fixp f' x == iter i f' (fixp f' x)).
induction i; [reflexivity |].
simpl; rewrite fixp_eq, IHi at 1; reflexivity.
etransitivity; [eapply fixp_eq|].
rewrite IHi at 1. reflexivity.
Qed.
(** Fixed points are unique, i.e. the fixp does not depend on the starting point of the iteration. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment