diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-18 23:22:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-18 23:22:32 +0100 |
commit | bc2c535af4288e06f285658ef2844aa45da9b302 (patch) | |
tree | 9e373cce6014b6d2b268c2aa9c8aceacb1c2156a /src/common | |
parent | 9403299d1a481ea4422524b6caa0d78e4c20fbaf (diff) | |
download | vericert-bc2c535af4288e06f285658ef2844aa45da9b302.tar.gz vericert-bc2c535af4288e06f285658ef2844aa45da9b302.zip |
Add new proofs about semantic identity
Diffstat (limited to 'src/common')
-rw-r--r-- | src/common/NonEmpty.v | 70 |
1 files changed, 69 insertions, 1 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index f15bb82..3aff11d 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -24,6 +24,8 @@ Require Export Coq.Classes.SetoidClass. Require Export Coq.Classes.SetoidDec. Require Import Coq.Logic.Decidable. +Require Import Vericertlib. + Inductive non_empty (A: Type) := | singleton : A -> non_empty A | cons : A -> non_empty A -> non_empty A @@ -214,7 +216,7 @@ Inductive norepet {A : Type} : non_empty A -> Prop := | list_norepet_cons hd tl : ~ In hd tl -> norepet tl -> norepet (hd ::| tl). -Lemma NEin_NEapp5 : +Lemma in_NEapp5 : forall A (a: A) x y, In a (app x y) -> In a x \/ In a y. @@ -224,3 +226,69 @@ Proof. - inv H. inv H1. left. constructor; tauto. apply IHx in H. inv H; intuition (constructor; auto). Qed. + +Lemma app_NEmap : + forall A B (f: A -> B) a b, + map f (app a b) = app (map f a) (map f b). +Proof. induction a; auto; intros; cbn in *; now rewrite IHa. Qed. + +Lemma of_list_some : + forall A a a' (e: A), + of_list a = Some a' -> + of_list (e :: a) = Some (cons e a'). +Proof. + induction a; [crush|]. + intros. + cbn in H. destruct a0. inv H. auto. + destruct_match; [|discriminate]. + inv H. specialize (IHa n a ltac:(trivial)). + cbn. destruct_match. unfold of_list in IHa. + fold (@of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. auto. + unfold of_list in IHa. fold (@of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. +Qed. + +Lemma of_list_contra : + forall A b (a: A), + ~ of_list (a :: b) = None. +Proof. + induction b; try solve [crush]. + intros. + specialize (IHb a). + enough (X: exists x, of_list (a :: b) = Some x). + inversion_clear X as [x X']. + erewrite of_list_some; eauto; discriminate. + destruct (of_list (a :: b)) eqn:?; [eauto|contradiction]. +Qed. + +Lemma of_list_exists : + forall A b (a: A), + exists x, of_list (a :: b) = Some x. +Proof. + intros. pose proof (of_list_contra _ b a). + destruct (of_list (a :: b)); try contradiction. + eauto. +Qed. + +Lemma of_list_exists2 : + forall A b (a c: A), + exists x, + of_list (c :: a :: b) = Some (cons c x) + /\ of_list (a :: b) = Some x. +Proof. + intros. pose proof (of_list_exists _ b a). + inversion_clear H as [x B]. + econstructor; split; eauto. + eapply of_list_some; eauto. +Qed. + +Lemma of_list_to_list : + forall A (x: list A) y, + of_list x = Some y -> + to_list y = x. +Proof. + induction x; [crush|]. + intros. destruct x; [crush|]. + pose proof (of_list_exists2 _ x a0 a). + inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H. + cbn. f_equal. eauto. +Qed. |