From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Jul 2011 08:26:16 +0000 Subject: Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) (limited to 'lib/Coqlib.v') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index f4d50e82..87b19ca8 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1285,3 +1285,46 @@ Qed. End DECIDABLE_PREDICATE. +(** * Well-founded orderings *) + +Require Import Relations. + +(** A non-dependent version of lexicographic ordering. *) + +Section LEX_ORDER. + +Variable A: Type. +Variable B: Type. +Variable ordA: A -> A -> Prop. +Variable ordB: B -> B -> Prop. + +Inductive lex_ord: A*B -> A*B -> Prop := + | lex_ord_left: forall a1 b1 a2 b2, + ordA a1 a2 -> lex_ord (a1,b1) (a2,b2) + | lex_ord_right: forall a b1 b2, + ordB b1 b2 -> lex_ord (a,b1) (a,b2). + +Lemma wf_lex_ord: + well_founded ordA -> well_founded ordB -> well_founded lex_ord. +Proof. + intros Awf Bwf. + assert (forall a, Acc ordA a -> forall b, Acc ordB b -> Acc lex_ord (a, b)). + induction 1. induction 1. constructor; intros. inv H3. + apply H0. auto. apply Bwf. + apply H2; auto. + red; intros. destruct a as [a b]. apply H; auto. +Qed. + +Lemma transitive_lex_ord: + transitive _ ordA -> transitive _ ordB -> transitive _ lex_ord. +Proof. + intros trA trB; red; intros. + inv H; inv H0. + left; eapply trA; eauto. + left; auto. + left; auto. + right; eapply trB; eauto. +Qed. + +End LEX_ORDER. + -- cgit