diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 13:33:32 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 13:33:32 +0100 |
| commit | 4290ead0dfdda0400dae528b66a38fe39dbbb18e (patch) | |
| tree | fec8638473548508a143650da99283656f7aee76 /src/common | |
| parent | 3e1aab82d0e14bdd120515a6e098c1c63e73427e (diff) | |
| download | vericert-4290ead0dfdda0400dae528b66a38fe39dbbb18e.tar.gz vericert-4290ead0dfdda0400dae528b66a38fe39dbbb18e.zip | |
Add check for mutexcl and fix top-level proof
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 762053a..cafa7ff 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -176,10 +176,14 @@ Proof. apply eqb_complete; auto. tauto. Qed. +Inductive Forall {A : Type} (P : A -> Prop) : non_empty A -> Prop := +| Forall_singleton a : P a -> Forall P (singleton a) +| Forall_cons x l : P x -> Forall P l -> Forall P (x ::| l). + Inductive Forall2 {A B : Type} (R : A -> B -> Prop) : non_empty A -> non_empty B -> Prop := - | Forall2_singleton : forall a b, R a b -> Forall2 R (singleton a) (singleton b) - | Forall2_cons : forall (x : A) (y : B) (l : non_empty A) (l' : non_empty B), - R x y -> Forall2 R l l' -> Forall2 R (x ::| l) (y ::| l'). +| Forall2_singleton : forall a b, R a b -> Forall2 R (singleton a) (singleton b) +| Forall2_cons : forall (x : A) (y : B) (l : non_empty A) (l' : non_empty B), + R x y -> Forall2 R l l' -> Forall2 R (x ::| l) (y ::| l'). Definition equivP {A R} `{Equivalence A R} n1 n2 := Forall2 R n1 n2. |