diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-06 19:24:10 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-07-26 15:59:55 +0200 |
commit | fd68e9d37164871cdcb4ee83ab649c5054b0f1cc (patch) | |
tree | 8bdd2ca790937a24a0354839da53ff39b0581772 /lib/Coqlib.v | |
parent | 39710f78062a4a999c079b58181a58e62b78c30b (diff) | |
download | compcert-fd68e9d37164871cdcb4ee83ab649c5054b0f1cc.tar.gz compcert-fd68e9d37164871cdcb4ee83ab649c5054b0f1cc.zip |
More lemmas about list append
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 1e93b91d..361ae924 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -773,6 +773,32 @@ Proof. exists (a0 :: l1); exists l2; intuition. simpl; congruence. Qed. +(** Properties of [List.app] (concatenation) *) + +Lemma list_append_injective_l: + forall (A: Type) (l1 l2 l1' l2': list A), + l1 ++ l2 = l1' ++ l2' -> List.length l1 = List.length l1' -> l1 = l1' /\ l2 = l2'. +Proof. + intros until l2'. revert l1 l1'. induction l1 as [ | a l1]; destruct l1' as [ | a' l1']; simpl; intros. +- auto. +- discriminate. +- discriminate. +- destruct (IHl1 l1'). congruence. congruence. split; congruence. +Qed. + +Lemma list_append_injective_r: + forall (A: Type) (l1 l2 l1' l2': list A), + l1 ++ l2 = l1' ++ l2' -> List.length l2 = List.length l2' -> l1 = l1' /\ l2 = l2'. +Proof. + intros. + assert (X: rev l2 = rev l2' /\ rev l1 = rev l1'). + { apply list_append_injective_l. + rewrite <- ! rev_app_distr. congruence. + rewrite ! rev_length; auto. } + rewrite <- (rev_involutive l1), <- (rev_involutive l1'), <- (rev_involutive l2), <- (rev_involutive l2'). + intuition congruence. +Qed. + (** Folding a function over a list *) Section LIST_FOLD. |