Confluence. It's not just a place where you can complain about colleagues to other colleagues.
It's also a property that is quite useful in many areas of CS!
As a reminder, a (non-deterministic) reduction relation --> is confluent if for every (multi-step) "peak"
u *<-- t -->* v (I use -->* for the multi-step version of -->) there is a corresponding "valley":
u -->* w *<-- v.
This basically says that your computation can't be "too"
| Set Implicit Arguments. | |
| (* On importe le module qui definit les listes *) | |
| Require Import List. | |
| Print list. | |
| Print option. | |
| (* Une section permet de declarer des Hypotheses et des Variables *) | |
| Section Typer. |
| Record Dial_2 := | |
| { | |
| U : Type; | |
| X : Type; | |
| alpha : U -> X -> Prop | |
| }. | |
| Record Mor (A B : Dial_2) := | |
| { | |
| f : U A -> U B; |
| Definition directed (D : Prop -> Prop) := | |
| (exists p, D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\ (q -> r). | |
| Definition finite (p : Prop) := | |
| forall D, directed D -> | |
| (p -> exists q, D q /\ q) ->exists q, D q /\ (p -> q). | |
| Lemma is_directed_with_p p : directed (fun q => ~q \/ (p /\ q)). |
| (* Cleanup and proofs of user11942s code *) | |
| Print sigT. | |
| Print sum. | |
| Print False. | |
| Print unit. |
| (* Sigma types *) | |
| (* Inductive Sigma (A:Set)(B:A -> Set) :Set := Spair: forall a:A, forall b : B a,Sigma A B. *) | |
| (* Definition E (A:Set)(B:A -> Set) (C: Sigma A B -> Set) (c: Sigma A B) *) | |
| (* (d: (forall x:A, forall y:B x, C (Spair A B x y))): C c := *) | |
| (* match c as c0 return (C c0) with *) | |
| (* | Spair a b => d a b *) | |
| (* end. *) |