Commit 35a2fcf8 authored by Martin Clochard's avatar Martin Clochard

example(wip): 2wp_gen, cont'd.

parent 4035a124
......@@ -95,6 +95,16 @@ module Set
end
(* Some usual big operators on sets. *)
module SetBigOps
use import Set
function bigunion (c:set (set 'a)) : set 'a = \x. exists s. c s /\ s x
function biginter (c:set (set 'a)) : set 'a = \x. forall s. c s -> s x
end
(* Basic definition on relations-as-arrows *)
module Rel
......
......@@ -2,13 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1000" memlimit="1"/>
<file name="../base.mlw">
<theory name="Fun" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FunExt" sum="74d4af5538daa9eb9ddee6284a05e5bf">
<goal name="WP_parameter extensional" expl="VC for extensional">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="FunCategory" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -19,36 +19,38 @@
<goal name="ext.1" expl="1.">
<transf name="inline_goal">
<goal name="ext.1.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</transf>
</goal>
<goal name="ext.2" expl="2.">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="neutral">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="FunExt.extensionality">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="FunCategory.assoc">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="FunCategory.neutral">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</theory>
<theory name="Set" sum="8dc39e2ae96fd0498b0d50bb47f235eb">
<goal name="sext_is_ext">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</theory>
<theory name="SetBigOps" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Rel" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RelExt" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -63,66 +65,66 @@
<goal name="extensionality">
<transf name="split_goal_wp">
<goal name="extensionality.1" expl="1.">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="extensionality.2" expl="2.">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="extensionality.3" expl="3.">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<transf name="compute_specified">
<goal name="assoc.1" expl="1.">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="reverse_antimorphism">
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="reverse_antimorphism_id">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="reverse_involution">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="neutral">
<transf name="compute_specified">
<goal name="neutral.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
</transf>
</goal>
<goal name="RelExt.extensionality">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.assoc">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism_id">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_involution">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.neutral">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</theory>
<theory name="SubsetOrder" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SetProofs" sum="0be5aa0fe01aa313571b5c5ef55cb77b">
<goal name="anti_subset">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="SubsetOrder.subset_order">
<proof prover="1"><result status="valid" time="0.02" steps="65"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
</theory>
<theory name="Image" sum="d41d8cd98f00b204e9800998ecf8427e">
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1000" memlimit="1"/>
<file name="../choice.mlw">
<theory name="Choice" sum="7c1ca533a0ae37f3bd6e59347ceef0bd">
<goal name="WP_parameter choose" expl="VC for choose">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter choose_if" expl="VC for choose_if">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1" steplimit="1" memlimit="1000"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
This diff is collapsed.
module Set use export base.Set end
module SubsetOrder use export base.SubsetOrder end
module SetBigOps use export base.SetBigOps end
\ No newline at end of file
......@@ -7,5 +7,7 @@
</theory>
<theory name="SubsetOrder" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="SetBigOps" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
......@@ -92,13 +92,14 @@ module Chain
predicate chain_complete (o:erel 'a) =
forall s. chain o s -> exists y. supremum o s y
(* quasi-chain-complete = all non-empty chains admit supremum. *)
predicate q_chain_complete (o:erel 'a) =
forall s inh. chain o s /\ s inh -> exists y. supremum o s y
predicate subchain (o:erel 'a) (s1 s2:set 'a) =
subset s1 s2 /\
forall x y. s1 x /\ s2 y /\ not s1 y -> o x y
function subchain_completion (c:set (set 'a)) : set 'a =
\x. exists s. c s /\ s x
predicate wf_chain (o:erel 'a) (s:set 'a) =
forall s2. subset s2 s /\ (exists x. s2 x) ->
exists y. minimum o s2 y
......@@ -162,13 +163,14 @@ end
module SubChain "W:non_conservative_extension:N" (* => SubChainProof *)
use export Chain
use import ho_set.SetBigOps
axiom subchain_complete_order : forall o:erel 'a.
transitive o -> order (subchain o) /\ chain_complete (subchain o)
axiom subchain_completion : forall o:erel 'a,ch.
chain (subchain o) ch ->
supremum (subchain o) ch (subchain_completion ch)
supremum (subchain o) ch (bigunion ch)
axiom chain_subchain_completion : forall o:erel 'a,ch x.
chain (subchain o) ch /\ (forall x. ch x -> chain o x) /\
......@@ -183,6 +185,7 @@ end
module SubChainProof
use import ho_set.SubsetOrder
use import ho_set.SetBigOps
use import Chain
lemma subchain_antisymetric : forall o:erel 'a.
......@@ -192,7 +195,7 @@ module SubChainProof
transitive o -> order (subchain o)
lemma subchain_completion : forall o:erel 'a,ch.
let u = subchain_completion ch in
let u = bigunion ch in
let sb = subchain o in
chain sb ch ->
supremum sb ch u
......@@ -211,7 +214,7 @@ module SubChainProof
chain (subchain o) ch /\
(forall x. ch x -> chain o x) /\ supremum (subchain o) ch x ->
chain o x
by x = subchain_completion ch
by x = bigunion ch
so forall u v. x u /\ x v -> o u v \/ o v u
by exists wu. ch wu /\ wu u
so exists wv. ch wv /\ wv v
......@@ -222,7 +225,7 @@ module SubChainProof
chain (subchain o) ch /\
(forall x. ch x -> wf_chain o x) /\ supremum (subchain o) ch x ->
wf_chain o x
by x = subchain_completion ch
by x = bigunion ch
so forall s2 y. s2 y /\ subset s2 x ->
(exists z. minimum o s2 z)
by exists wy. ch wy /\ wy y
......@@ -347,4 +350,13 @@ module ProductChain
so exists y. supremum o2 (image snd ch) y
so supremum (rprod o1 o2) ch (x,y)
lemma prod_q_chain_complete : forall o1:erel 'a,o2:erel 'b.
order o1 /\ order o2 /\ q_chain_complete o1 /\ q_chain_complete o2 ->
q_chain_complete (rprod o1 o2)
by forall ch inh. chain (rprod o1 o2) ch /\ ch inh ->
let (a,b) = inh in image fst ch a /\ image snd ch b
so exists x. supremum o1 (image fst ch) x
so exists y. supremum o2 (image snd ch) y
so supremum (rprod o1 o2) ch (x,y)
end
\ No newline at end of file
......@@ -37,7 +37,7 @@ module Iterates "W:non_conservative_extension:N" (* => IterateProof *)
function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) 'a : 'a
axiom tr_reach_maximum : forall o f,x:'a.
order o /\ inflationary o f /\ chain_complete o ->
order o /\ inflationary o f /\ q_chain_complete o ->
f (fixpoint_above o f x) = fixpoint_above o f x /\
maximum o (tr_reach o f x) (fixpoint_above o f x)
......@@ -109,11 +109,12 @@ module IterateProof
sup o (tr_reach o f u)
lemma fixpoint_max_proof : forall o f,u:'a.
order o /\ chain_complete o /\ inflationary o f ->
order o /\ q_chain_complete o /\ inflationary o f ->
(forall x y. tr_reach o f u x /\ tr_reach o f u y ->
separator o f x y && (o x y \/ o y x)) &&
chain o (tr_reach o f u) && let y = fixpoint_above o f u in
maximum o (tr_reach o f u) y && (f y = y by o (f y) y /\ o y (f y))
(maximum o (tr_reach o f u) y by tr_reach o f u u)
&& (f y = y by o (f y) y /\ o y (f y))
lemma fixpoint_is_max_proof : forall o f,x y:'a.
order o /\ inflationary o f /\ tr_reach o f x y /\ f y = y ->
......
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