diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
commit | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (patch) | |
tree | 01c04d7e5770d4e927da40052f17eff48e7d8079 /src/common | |
parent | 9134c30e5c9a46299aacc94dd5664308bd554303 (diff) | |
download | vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.tar.gz vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.zip |
Finish mutual exclusivity check
Diffstat (limited to 'src/common')
-rw-r--r-- | src/common/NonEmpty.v | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 24a29a3..01456d0 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -97,7 +97,7 @@ Inductive In {A: Type} (x: A) : non_empty A -> Prop := Ltac inv X := inversion X; clear X; subst. -Lemma in_dec: +Definition in_dec: forall A (a: A) (l: non_empty A), (forall a b: A, {a = b} + {a <> b}) -> {In a l} + {~ In a l}. @@ -338,3 +338,31 @@ Proof. + exists a; split; auto; constructor; tauto. + exploit IHn; eauto; simplify. exists x0; split; auto; constructor; tauto. Qed. + +Fixpoint norepet_check {A} eq_dec (ne: non_empty A) := + match ne with + | singleton a => true + | a ::| b => + if in_dec A a b eq_dec then false + else norepet_check eq_dec b + end. + +Lemma norepet_check_correct : + forall A eq_dec ne, + @norepet_check A eq_dec ne = true -> + norepet ne. +Proof. + induction ne; intros; [constructor|]. + cbn in H. destruct_match; [discriminate|]. + constructor; auto. +Qed. + +Lemma to_list_in : + forall A ne (x: A), + In x ne -> + List.In x (to_list ne). +Proof. + induction ne. + - intros. inv H. cbn; tauto. + - intros; cbn. inv H. inv H1; eauto. +Qed. |