From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 29 Nov 2003 17:28:49 +0000 Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sorting/Sorting.v | 144 +++++++++++++++++++++++---------------------- 1 file changed, 75 insertions(+), 69 deletions(-) (limited to 'theories/Sorting/Sorting.v') diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index cad4e20198..b1986d4e74 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -8,110 +8,116 @@ (*i $Id$ i*) -Require PolyList. -Require Multiset. -Require Permutation. -Require Relations. +Require Import List. +Require Import Multiset. +Require Import Permutation. +Require Import Relations. Set Implicit Arguments. Section defs. Variable A : Set. -Variable leA : (relation A). -Variable eqA : (relation A). +Variable leA : relation A. +Variable eqA : relation A. -Local gtA := [x,y:A]~(leA x y). +Let gtA (x y:A) := ~ leA x y. -Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}. -Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. -Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y). -Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z). -Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y). +Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}. +Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. +Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y. +Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. +Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. -Hints Resolve leA_refl. -Hints Immediate eqA_dec leA_dec leA_antisym. +Hint Resolve leA_refl. +Hint Immediate eqA_dec leA_dec leA_antisym. -Local emptyBag := (EmptyBag A). -Local singletonBag := (SingletonBag eqA_dec). +Let emptyBag := EmptyBag A. +Let singletonBag := SingletonBag _ eqA_dec. (** [lelistA] *) -Inductive lelistA [a:A] : (list A) -> Prop := - nil_leA : (lelistA a (nil A)) - | cons_leA : (b:A)(l:(list A))(leA a b)->(lelistA a (cons b l)). -Hint constr_lelistA := Constructors lelistA. +Inductive lelistA (a:A) : list A -> Prop := + | nil_leA : lelistA a nil + | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l). +Hint Constructors lelistA. -Lemma lelistA_inv : (a,b:A)(l:(list A)) - (lelistA a (cons b l)) -> (leA a b). +Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b. Proof. - Intros; Inversion H; Trivial with datatypes. + intros; inversion H; trivial with datatypes. Qed. (** definition for a list to be sorted *) -Inductive sort : (list A) -> Prop := - nil_sort : (sort (nil A)) - | cons_sort : (a:A)(l:(list A))(sort l) -> (lelistA a l) -> (sort (cons a l)). -Hint constr_sort := Constructors sort. +Inductive sort : list A -> Prop := + | nil_sort : sort nil + | cons_sort : + forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l). +Hint Constructors sort. -Lemma sort_inv : (a:A)(l:(list A))(sort (cons a l))->(sort l) /\ (lelistA a l). +Lemma sort_inv : + forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l. Proof. -Intros; Inversion H; Auto with datatypes. +intros; inversion H; auto with datatypes. Qed. -Lemma sort_rec : (P:(list A)->Set) - (P (nil A)) -> - ((a:A)(l:(list A))(sort l)->(P l)->(lelistA a l)->(P (cons a l))) -> - (y:(list A))(sort y) -> (P y). +Lemma sort_rec : + forall P:list A -> Set, + P nil -> + (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) -> + forall y:list A, sort y -> P y. Proof. -Induction y; Auto with datatypes. -Intros; Elim (!sort_inv a l); Auto with datatypes. +simple induction y; auto with datatypes. +intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes. Qed. (** merging two sorted lists *) -Inductive merge_lem [l1:(list A);l2:(list A)] : Set := - merge_exist : (l:(list A))(sort l) -> - (meq (list_contents eqA_dec l) - (munion (list_contents eqA_dec l1) (list_contents eqA_dec l2))) -> - ((a:A)(lelistA a l1)->(lelistA a l2)->(lelistA a l)) -> - (merge_lem l1 l2). - -Lemma merge : (l1:(list A))(sort l1)->(l2:(list A))(sort l2)->(merge_lem l1 l2). +Inductive merge_lem (l1 l2:list A) : Set := + merge_exist : + forall l:list A, + sort l -> + meq (list_contents _ eqA_dec l) + (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> + (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) -> + merge_lem l1 l2. + +Lemma merge : + forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2. Proof. - Induction 1; Intros. - Apply merge_exist with l2; Auto with datatypes. - Elim H3; Intros. - Apply merge_exist with (cons a l); Simpl; Auto with datatypes. - Elim (leA_dec a a0); Intros. + simple induction 1; intros. + apply merge_exist with l2; auto with datatypes. + elim H3; intros. + apply merge_exist with (a :: l); simpl in |- *; auto with datatypes. + elim (leA_dec a a0); intros. (* 1 (leA a a0) *) - Cut (merge_lem l (cons a0 l0)); Auto with datatypes. - Intros (l3, l3sorted, l3contents, Hrec). - Apply merge_exist with (cons a l3); Simpl; Auto with datatypes. - Apply meq_trans with (munion (singletonBag a) - (munion (list_contents eqA_dec l) - (list_contents eqA_dec (cons a0 l0)))). - Apply meq_right; Trivial with datatypes. - Apply meq_sym; Apply munion_ass. - Intros; Apply cons_leA. - Apply lelistA_inv with l; Trivial with datatypes. + cut (merge_lem l (a0 :: l0)); auto with datatypes. + intros [l3 l3sorted l3contents Hrec]. + apply merge_exist with (a :: l3); simpl in |- *; auto with datatypes. + apply meq_trans with + (munion (singletonBag a) + (munion (list_contents _ eqA_dec l) + (list_contents _ eqA_dec (a0 :: l0)))). + apply meq_right; trivial with datatypes. + apply meq_sym; apply munion_ass. + intros; apply cons_leA. + apply lelistA_inv with l; trivial with datatypes. (* 2 (leA a0 a) *) - Elim H5; Simpl; Intros. - Apply merge_exist with (cons a0 l3); Simpl; Auto with datatypes. - Apply meq_trans with (munion (singletonBag a0) - (munion (munion (singletonBag a) - (list_contents eqA_dec l)) - (list_contents eqA_dec l0))). - Apply meq_right; Trivial with datatypes. - Apply munion_perm_left. - Intros; Apply cons_leA; Apply lelistA_inv with l0; Trivial with datatypes. + elim H5; simpl in |- *; intros. + apply merge_exist with (a0 :: l3); simpl in |- *; auto with datatypes. + apply meq_trans with + (munion (singletonBag a0) + (munion (munion (singletonBag a) (list_contents _ eqA_dec l)) + (list_contents _ eqA_dec l0))). + apply meq_right; trivial with datatypes. + apply munion_perm_left. + intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes. Qed. End defs. Unset Implicit Arguments. -Hint constr_sort : datatypes v62 := Constructors sort. -Hint constr_lelistA : datatypes v62 := Constructors lelistA. +Hint Constructors sort: datatypes v62. +Hint Constructors lelistA: datatypes v62. \ No newline at end of file -- cgit v1.2.3