Changeset 2949 for src/utilities

Timestamp:

Mar 25, 2013, 9:48:01 PM (8 years ago)

Author:

sacerdot

Message:

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

File:

• src/utilities/fixpoints.ma (modified) (1 diff)

src/utilities/fixpoints.ma

@@ -13 +13 @@
 definition equations ≝ λlatt : property_lattice.label → rhs latt.
 
-record fixpoint (latt : property_lattice) : Type[0] ≝
-{ fix_lfp :1> equations latt → valuation latt
+record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝
+{ fix_lfp :> valuation latt
 ; fix_correct :
-  ∀eqs : equations latt.
-  let sol ≝ fix_lfp eqs in
   ∀l : label.
-  l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *)
+   (* inclusion suffices for correctness *)
+   l_included latt (eqs l fix_lfp) (fix_lfp l)
 }.
 
-definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
+definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs.
+
+coercion apply_fixpoint:
+ ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝
+ λlatt,eqs,f,l. fix_lfp … f l
+ on _f: fixpoint ? ? to label → ?.