diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /lib/Coqlib.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
download | compcert-355b4abcee015c3fae9ac5653c25259e104a886c.tar.gz compcert-355b4abcee015c3fae9ac5653c25259e104a886c.zip |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 184fe28f..7bee366b 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -23,6 +23,8 @@ Axiom proof_irrelevance: (** * Useful tactics *) +Ltac inv H := inversion H; clear H; subst. + Ltac predSpec pred predspec x y := generalize (predspec x y); case (pred x y); intro. @@ -753,6 +755,44 @@ Proof. generalize list_norepet_app; firstorder. Qed. +(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *) + +Inductive is_tail (A: Set): list A -> list A -> Prop := + | is_tail_refl: + forall c, is_tail c c + | is_tail_cons: + forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2). + +Lemma is_tail_in: + forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2. +Proof. + induction c2; simpl; intros. + inversion H. + inversion H. tauto. right; auto. +Qed. + +Lemma is_tail_cons_left: + forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2. +Proof. + induction c2; intros; inversion H. + constructor. constructor. constructor. auto. +Qed. + +Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. + +Lemma is_tail_incl: + forall (A: Set) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2. +Proof. + induction 1; eauto with coqlib. +Qed. + +Lemma is_tail_trans: + forall (A: Set) (l1 l2: list A), + is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3. +Proof. + induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto. +Qed. + (** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and [P xi yi] holds for all [i]. *) |