KevinMidboe/linguist
1
0
Fork 0
mirror of https://github.com/KevinMidboe/linguist.git synced 2025-10-29 17:50:22 +00:00
Code Issues Packages Projects Releases Wiki Activity

Delete GPL2.1-licensed Coq samples

Browse Source 
These files are modified variants of the ones included in Coq's standard
distribution. The original materials feature the GPL 2.1 license in each
file's header, which was suspiciously removed from Linguist's samples.

    https://github.com/coq/coq/tree/trunk/theories

Basics.v is a different file to that found in Coq's distro, but is vague
in origin and being removed to err on the side of caution. The remaining
samples are from a MIT-licensed online course by Software Foundations:

    https://www.cis.upenn.edu/~bcpierce/sf/current/

References: github/linguist#3313
This commit is contained in:
Alhadis
2016-11-03 02:15:36 +11:00
parent 417239004a
commit 85c9833081
6 changed files with 0 additions and 2589 deletions
Download Patch File Download Diff File Expand all files Collapse all files

707
samples/Coq/Basics.v
View File

@@ -1,707 +0,0 @@
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
Inductive bool : Type :=
| true : bool
| false : bool.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
Definition nandb (b1: bool) (b2:bool) : bool :=
match b1 with
| true => match b2 with
| false => true
| true => false
end
| false => true
end.
Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.
Definition andb3 (b1: bool) (b2:bool) (b3:bool) : bool :=
match b1 with
| false => false
| true => match b2 with
| false => false
| true => b3
end
end.
Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.
Module Playground1.
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Fixpoint evenb (n : nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Definition oddb (n : nat) : bool := negb (evenb n).
Example test_oddb1: (oddb (S O)) = true.
Proof. reflexivity. Qed.
Example test_oddb2: (oddb (S (S (S (S O))))) = false.
Proof. reflexivity. Qed.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Fixpoint minus (n m : nat) : nat :=
match n, m with
| O, _ => n
| S n', O => S n'
| S n', S m' => minus n' m'
end.
Fixpoint exp (base power : nat) : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
Fixpoint factorial (n : nat) : nat :=
match n with
| O => S O
| S n' => mult n (factorial n')
end.
Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
Proof. simpl. reflexivity. Qed.
Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.
Fixpoint beq_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
Fixpoint ble_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
Proof. simpl. reflexivity. Qed.
Definition blt_nat (n m : nat) : bool :=
(andb (negb (beq_nat n m)) (ble_nat n m)).
Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
Proof. simpl. reflexivity. Qed.
Theorem plus_O_n : forall n : nat, O + n = n.
Proof.
simpl. reflexivity. Qed.
Theorem plus_O_n' : forall n : nat, O + n = n.
Proof.
reflexivity. Qed.
Theorem plus_O_n'' : forall n : nat, O + n = n.
Proof.
intros n. reflexivity. Qed.
Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_1: forall n : nat, O * n = O.
Proof.
intros n. reflexivity. Qed.
Theorem plus_id_example : forall n m:nat,
n = m -> n + n = m + m.
Proof.
intros n m.
intros H.
rewrite -> H.
reflexivity. Qed.
Theorem plus_id_exercise : forall n m o: nat,
n = m -> m = o -> n + m = m + o.
Proof.
intros n m o.
intros H.
intros H'.
rewrite -> H.
rewrite <- H'.
reflexivity.
Qed.
Theorem mult_0_plus : forall n m : nat,
(O + n) * m = n * m.
Proof.
intros n m.
rewrite -> plus_O_n.
reflexivity. Qed.
Theorem mult_1_plus : forall n m: nat,
((S O) + n) * m = m + (n * m).
Proof.
intros n m.
rewrite -> plus_1_1.
reflexivity.
Qed.
Theorem mult_1 : forall n : nat,
n * (S O) = n.
Proof.
intros n.
induction n as [| n'].
reflexivity.
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
Theorem plus_1_neq_0 : forall n : nat,
beq_nat (n + (S O)) O = false.
Proof.
intros n.
destruct n as [| n'].
reflexivity.
reflexivity.
Qed.
Theorem zero_nbeq_plus_1 : forall n : nat,
beq_nat O (n + (S O)) = false.
Proof.
intros n.
destruct n.
reflexivity.
reflexivity.
Qed.
Require String. Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.
Ltac SSCase name := Case_aux SSCase name.
Ltac SSSCase name := Case_aux SSSCase name.
Ltac SSSSCase name := Case_aux SSSSCase name.
Ltac SSSSSCase name := Case_aux SSSSSCase name.
Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
Theorem andb_true_elim1 : forall b c : bool,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity. Qed.
Theorem plus_0_r : forall n : nat, n + O = n.
Proof.
intros n. induction n as [| n'].
Case "n = 0". reflexivity.
Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
Theorem minus_diag : forall n,
minus n n = O.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
simpl. reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity. Qed.
Theorem mult_0_r : forall n:nat,
n * O = O.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity. Qed.
Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Proof.
intros n m. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity. Qed.
Theorem plus_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p.
induction n as [| n'].
reflexivity.
simpl.
rewrite -> IHn'.
reflexivity. Qed.
Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
Proof.
intros n m. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity. Qed.
Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
Proof.
intros n m.
induction n as [| n'].
reflexivity.
reflexivity.
Qed.
Theorem plus_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m.
induction n as [| n'].
Case "n = 0".
simpl.
rewrite -> plus_0_r.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
rewrite -> plus_distr.
reflexivity. Qed.
Fixpoint double (n:nat) :=
match n with
| O => O
| S n' => S (S (double n'))
end.
Lemma double_plus : forall n, double n = n + n.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'.
rewrite -> plus_distr. reflexivity.
Qed.
Theorem beq_nat_refl : forall n : nat,
true = beq_nat n n.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n".
simpl. rewrite <- IHn'.
reflexivity. Qed.
Theorem plus_rearrange: forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
assert(H: n + m = m + n).
Case "Proof by assertion".
rewrite -> plus_comm. reflexivity.
rewrite -> H. reflexivity. Qed.
Theorem plus_swap : forall n m p: nat,
n + (m + p) = m + (n + p).
Proof.
intros n m p.
rewrite -> plus_assoc.
assert(H: m + (n + p) = (m + n) + p).
rewrite -> plus_assoc.
reflexivity.
rewrite -> H.
assert(H2: m + n = n + m).
rewrite -> plus_comm.
reflexivity.
rewrite -> H2.
reflexivity.
Qed.
Theorem plus_swap' : forall n m p: nat,
n + (m + p) = m + (n + p).
Proof.
intros n m p.
rewrite -> plus_assoc.
assert(H: m + (n + p) = (m + n) + p).
rewrite -> plus_assoc.
reflexivity.
rewrite -> H.
replace (m + n) with (n + m).
rewrite -> plus_comm.
reflexivity.
rewrite -> plus_comm.
reflexivity.
Qed.
Theorem mult_1_distr: forall m n: nat,
n * ((S O) + m) = n * (S O) + n * m.
Proof.
intros n m.
rewrite -> mult_1.
rewrite -> plus_1_1.
simpl.
induction m as [|m'].
simpl.
reflexivity.
simpl.
rewrite -> plus_swap.
rewrite <- IHm'.
reflexivity.
Qed.
Theorem mult_comm: forall m n : nat,
m * n = n * m.
Proof.
intros m n.
induction n as [| n'].
Case "n = 0".
simpl.
rewrite -> mult_0_r.
reflexivity.
Case "n = S n'".
simpl.
rewrite <- mult_distr.
rewrite -> mult_1_distr.
rewrite -> mult_1.
rewrite -> IHn'.
reflexivity.
Qed.
Theorem evenb_next : forall n : nat,
evenb n = evenb (S (S n)).
Proof.
intros n.
Admitted.
Theorem negb_negb : forall n : bool,
n = negb (negb n).
Proof.
intros n.
destruct n.
reflexivity.
reflexivity.
Qed.
Theorem evenb_n_oddb_Sn : forall n : nat,
evenb n = negb (evenb (S n)).
Proof.
intros n.
induction n as [|n'].
reflexivity.
assert(H: evenb n' = evenb (S (S n'))).
reflexivity.
rewrite <- H.
rewrite -> IHn'.
rewrite <- negb_negb.
reflexivity.
Qed.
(*Fixpoint bad (n : nat) : bool :=
match n with
| O => true
| S O => bad (S n)
| S (S n') => bad n'
end.*)
Theorem ble_nat_refl : forall n:nat,
true = ble_nat n n.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
reflexivity.
Case "n = S n".
simpl.
rewrite <- IHn'.
reflexivity.
Qed.
Theorem zero_nbeq_S : forall n: nat,
beq_nat O (S n) = false.
Proof.
intros n.
reflexivity.
Qed.
Theorem andb_false_r : forall b : bool,
andb b false = false.
Proof.
intros b.
destruct b.
reflexivity.
reflexivity.
Qed.
Theorem plus_ble_compat_1 : forall n m p : nat,
ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
Proof.
intros n m p.
intros H.
induction p.
Case "p = 0".
simpl.
rewrite -> H.
reflexivity.
Case "p = S p'".
simpl.
rewrite -> IHp.
reflexivity.
Qed.
Theorem S_nbeq_0 : forall n:nat,
beq_nat (S n) O = false.
Proof.
intros n.
reflexivity.
Qed.
Theorem mult_1_1 : forall n:nat, (S O) * n = n.
Proof.
intros n.
simpl.
rewrite -> plus_0_r.
reflexivity. Qed.
Theorem all3_spec : forall b c : bool,
orb (andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
intros b c.
destruct b.
destruct c.
reflexivity.
reflexivity.
reflexivity.
Qed.
Lemma mult_plus_1 : forall n m : nat,
S(m + n) = m + (S n).
Proof.
intros n m.
induction m.
reflexivity.
simpl.
rewrite -> IHm.
reflexivity.
Qed.
Theorem mult_mult : forall n m : nat,
n * (S m) = n * m + n.
Proof.
intros n m.
induction n.
reflexivity.
simpl.
rewrite -> IHn.
rewrite -> plus_assoc.
rewrite -> mult_plus_1.
reflexivity.
Qed.
Theorem mult_plus_distr_r : forall n m p:nat,
(n + m) * p = (n * p) + (m * p).
Proof.
intros n m p.
induction p.
rewrite -> mult_0_r.
rewrite -> mult_0_r.
rewrite -> mult_0_r.
reflexivity.
rewrite -> mult_mult.
rewrite -> mult_mult.
rewrite -> mult_mult.
rewrite -> IHp.
assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
rewrite <- plus_assoc.
reflexivity.
rewrite -> H1.
assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
rewrite -> plus_swap.
reflexivity.
rewrite -> H2.
assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
rewrite -> plus_assoc.
reflexivity.
rewrite -> H3.
reflexivity.
Qed.
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
intros n m p.
induction n.
simpl.
reflexivity.
simpl.
rewrite -> mult_plus_distr_r.
rewrite -> IHn.
reflexivity.
Qed.
Inductive bin : Type :=
| BO : bin
| D : bin -> bin
| M : bin -> bin.
Fixpoint incbin (n : bin) : bin :=
match n with
| BO => M (BO)
| D n' => M n'
| M n' => D (incbin n')
end.
Fixpoint bin2un (n : bin) : nat :=
match n with
| BO => O
| D n' => double (bin2un n')
| M n' => S (double (bin2un n'))
end.
Theorem bin_comm : forall n : bin,
bin2un(incbin n) = S (bin2un n).
Proof.
intros n.
induction n.
reflexivity.
reflexivity.
simpl.
rewrite -> IHn.
reflexivity.
Qed.
End Playground1.

290
samples/Coq/Heap.v
View File

@@ -1,290 +0,0 @@
(** A development of Treesort on Heap trees. It has an average
complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
the list is already sorted) *)
(* G. Huet 1-9-95 uses Multiset *)
Require Import List Multiset PermutSetoid Relations Sorting.
Section defs.
(** * Trees and heap trees *)
(** ** Definition of trees over an ordered set *)
Variable A : Type.
Variable leA : relation A.
Variable eqA : relation A.
Let gtA (x y:A) := ~ leA 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.
Hint Resolve leA_refl.
Hint Immediate eqA_dec leA_dec leA_antisym.
Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.
Inductive Tree :=
| Tree_Leaf : Tree
| Tree_Node : A -> Tree -> Tree -> Tree.
(** [a] is lower than a Tree [T] if [T] is a Leaf
or [T] is a Node holding [b>a] *)
Definition leA_Tree (a:A) (t:Tree) :=
match t with
| Tree_Leaf => True
| Tree_Node b T1 T2 => leA a b
end.
Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
Proof.
simpl; auto with datatypes.
Qed.
Lemma leA_Tree_Node :
forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
Proof.
simpl; auto with datatypes.
Qed.
(** ** The heap property *)
Inductive is_heap : Tree -> Prop :=
| nil_is_heap : is_heap Tree_Leaf
| node_is_heap :
forall (a:A) (T1 T2:Tree),
leA_Tree a T1 ->
leA_Tree a T2 ->
is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
Lemma invert_heap :
forall (a:A) (T1 T2:Tree),
is_heap (Tree_Node a T1 T2) ->
leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
Proof.
intros; inversion H; auto with datatypes.
Qed.
(* This lemma ought to be generated automatically by the Inversion tools *)
Lemma is_heap_rect :
forall P:Tree -> Type,
P Tree_Leaf ->
(forall (a:A) (T1 T2:Tree),
leA_Tree a T1 ->
leA_Tree a T2 ->
is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T:Tree, is_heap T -> P T.
Proof.
simple induction T; auto with datatypes.
intros a G PG D PD PN.
elim (invert_heap a G D); auto with datatypes.
intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
apply X0; auto with datatypes.
Qed.
(* This lemma ought to be generated automatically by the Inversion tools *)
Lemma is_heap_rec :
forall P:Tree -> Set,
P Tree_Leaf ->
(forall (a:A) (T1 T2:Tree),
leA_Tree a T1 ->
leA_Tree a T2 ->
is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T:Tree, is_heap T -> P T.
Proof.
simple induction T; auto with datatypes.
intros a G PG D PD PN.
elim (invert_heap a G D); auto with datatypes.
intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
apply X; auto with datatypes.
Qed.
Lemma low_trans :
forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
Proof.
simple induction T; auto with datatypes.
intros; simpl; apply leA_trans with b; auto with datatypes.
Qed.
(** ** Merging two sorted lists *)
Inductive merge_lem (l1 l2:list A) : Type :=
merge_exist :
forall l:list A,
Sorted leA l ->
meq (list_contents _ eqA_dec l)
(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
(forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
merge_lem l1 l2.
Require Import Morphisms.
Instance: Equivalence (@meq A).
Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
Lemma merge :
forall l1:list A, Sorted leA l1 ->
forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
Proof.
fix 1; intros; destruct l1.
apply merge_exist with l2; auto with datatypes.
rename l1 into l.
revert l2 H0. fix 1. intros.
destruct l2 as [|a0 l0].
apply merge_exist with (a :: l); simpl; auto with datatypes.
elim (leA_dec a a0); intros.
(* 1 (leA a a0) *)
apply Sorted_inv in H. destruct H.
destruct (merge l H (a0 :: l0) H0).
apply merge_exist with (a :: l1). clear merge merge0.
auto using cons_sort, cons_leA with datatypes.
simpl. rewrite m. now rewrite munion_ass.
intros. apply cons_leA.
apply (@HdRel_inv _ leA) with l; trivial with datatypes.
(* 2 (leA a0 a) *)
apply Sorted_inv in H0. destruct H0.
destruct (merge0 l0 H0). clear merge merge0.
apply merge_exist with (a0 :: l1);
auto using cons_sort, cons_leA with datatypes.
simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
intros. apply cons_leA.
apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
Qed.
(** ** From trees to multisets *)
(** contents of a tree as a multiset *)
(** Nota Bene : In what follows the definition of SingletonBag
in not used. Actually, we could just take as postulate:
[Parameter SingletonBag : A->multiset]. *)
Fixpoint contents (t:Tree) : multiset A :=
match t with
| Tree_Leaf => emptyBag
| Tree_Node a t1 t2 =>
munion (contents t1) (munion (contents t2) (singletonBag a))
end.
(** equivalence of two trees is equality of corresponding multisets *)
Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
(** * From lists to sorted lists *)
(** ** Specification of heap insertion *)
Inductive insert_spec (a:A) (T:Tree) : Type :=
insert_exist :
forall T1:Tree,
is_heap T1 ->
meq (contents T1) (munion (contents T) (singletonBag a)) ->
(forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
insert_spec a T.
Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
Proof.
simple induction 1; intros.
apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
simpl; unfold meq, munion; auto using node_is_heap with datatypes.
elim (leA_dec a a0); intros.
elim (X a0); intros.
apply insert_exist with (Tree_Node a T2 T0);
auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
simpl; apply treesort_twist1; trivial with datatypes.
elim (X a); intros T3 HeapT3 ConT3 LeA.
apply insert_exist with (Tree_Node a0 T2 T3);
auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
apply low_trans with a; auto with datatypes.
apply LeA; auto with datatypes.
apply low_trans with a; auto with datatypes.
simpl; apply treesort_twist2; trivial with datatypes.
Qed.
(** ** Building a heap from a list *)
Inductive build_heap (l:list A) : Type :=
heap_exist :
forall T:Tree,
is_heap T ->
meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
Lemma list_to_heap : forall l:list A, build_heap l.
Proof.
simple induction l.
apply (heap_exist nil Tree_Leaf); auto with datatypes.
simpl; unfold meq; exact nil_is_heap.
simple induction 1.
intros T i m; elim (insert T i a).
intros; apply heap_exist with T1; simpl; auto with datatypes.
apply meq_trans with (munion (contents T) (singletonBag a)).
apply meq_trans with (munion (singletonBag a) (contents T)).
apply meq_right; trivial with datatypes.
apply munion_comm.
apply meq_sym; trivial with datatypes.
Qed.
(** ** Building the sorted list *)
Inductive flat_spec (T:Tree) : Type :=
flat_exist :
forall l:list A,
Sorted leA l ->
(forall a:A, leA_Tree a T -> HdRel leA a l) ->
meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
Proof.
intros T h; elim h; intros.
apply flat_exist with (nil (A:=A)); auto with datatypes.
elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
elim (merge _ s1 _ s2); intros.
apply flat_exist with (a :: l); simpl; auto with datatypes.
apply meq_trans with
(munion (list_contents _ eqA_dec l1)
(munion (list_contents _ eqA_dec l2) (singletonBag a))).
apply meq_congr; auto with datatypes.
apply meq_trans with
(munion (singletonBag a)
(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
apply munion_rotate.
apply meq_right; apply meq_sym; trivial with datatypes.
Qed.
(** * Specification of treesort *)
Theorem treesort :
forall l:list A,
{m : list A | Sorted leA m & permutation _ eqA_dec l m}.
Proof.
intro l; unfold permutation.
elim (list_to_heap l).
intros.
elim (heap_to_list T); auto with datatypes.
intros.
exists l0; auto with datatypes.
apply meq_trans with (contents T); trivial with datatypes.
Qed.
End defs.

539
samples/Coq/PermutSetoid.v
View File

@@ -1,539 +0,0 @@
Require Import Omega Relations Multiset SetoidList.
(** This file is deprecated, use [Permutation.v] instead.
Indeed, this file defines a notion of permutation based on
multisets (there exists a permutation between two lists iff every
elements have the same multiplicity in the two lists) which
requires a more complex apparatus (the equipment of the domain
with a decidable equality) than [Permutation] in [Permutation.v].
The relation between the two relations are in lemma
[permutation_Permutation].
File [Permutation] concerns Leibniz equality : it shows in particular
that [List.Permutation] and [permutation] are equivalent in this context.
*)
Set Implicit Arguments.
Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
Section Permut.
(** * From lists to multisets *)
Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.
(** contents of a list *)
Fixpoint list_contents (l:list A) : multiset A :=
match l with
| [] => emptyBag
| a :: l => munion (singletonBag a) (list_contents l)
end.
Lemma list_contents_app :
forall l m:list A,
meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
Proof.
simple induction l; simpl; auto with datatypes.
intros.
apply meq_trans with
(munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
auto with datatypes.
Qed.
(** * [permutation]: definition and basic properties *)
Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
Lemma permut_refl : forall l:list A, permutation l l.
Proof.
unfold permutation; auto with datatypes.
Qed.
Lemma permut_sym :
forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
Proof.
unfold permutation, meq; intros; symmetry; trivial.
Qed.
Lemma permut_trans :
forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
Proof.
unfold permutation; intros.
apply meq_trans with (list_contents m); auto with datatypes.
Qed.
Lemma permut_cons_eq :
forall l m:list A,
permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
Proof.
unfold permutation; simpl; intros.
apply meq_trans with (munion (singletonBag a') (list_contents l)).
apply meq_left, meq_singleton; auto.
auto with datatypes.
Qed.
Lemma permut_cons :
forall l m:list A,
permutation l m -> forall a:A, permutation (a :: l) (a :: m).
Proof.
unfold permutation; simpl; auto with datatypes.
Qed.
Lemma permut_app :
forall l l' m m':list A,
permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
Proof.
unfold permutation; intros.
apply meq_trans with (munion (list_contents l) (list_contents m));
auto using permut_cons, list_contents_app with datatypes.
apply meq_trans with (munion (list_contents l') (list_contents m'));
auto using permut_cons, list_contents_app with datatypes.
apply meq_trans with (munion (list_contents l') (list_contents m));
auto using permut_cons, list_contents_app with datatypes.
Qed.
Lemma permut_add_inside_eq :
forall a a' l1 l2 l3 l4, eqA a a' ->
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
Proof.
unfold permutation, meq in *; intros.
specialize H0 with a0.
repeat rewrite list_contents_app in *; simpl in *.
destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
do 2 rewrite <- plus_n_Sm; f_equal; auto.
Qed.
Lemma permut_add_inside :
forall a l1 l2 l3 l4,
permutation (l1 ++ l2) (l3 ++ l4) ->
permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
Proof.
unfold permutation, meq in *; intros.
generalize (H a0); clear H.
do 4 rewrite list_contents_app.
simpl.
destruct (eqA_dec a a0); simpl; auto with arith.
do 2 rewrite <- plus_n_Sm; f_equal; auto.
Qed.
Lemma permut_add_cons_inside_eq :
forall a a' l l1 l2, eqA a a' ->
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a' :: l2).
Proof.
intros;
replace (a :: l) with ([] ++ a :: l); trivial;
apply permut_add_inside_eq; trivial.
Qed.
Lemma permut_add_cons_inside :
forall a l l1 l2,
permutation l (l1 ++ l2) ->
permutation (a :: l) (l1 ++ a :: l2).
Proof.
intros;
replace (a :: l) with ([] ++ a :: l); trivial;
apply permut_add_inside; trivial.
Qed.
Lemma permut_middle :
forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
Proof.
intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
Qed.
Lemma permut_sym_app :
forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
Proof.
intros l1 l2;
unfold permutation, meq;
intro a; do 2 rewrite list_contents_app; simpl;
auto with arith.
Qed.
Lemma permut_rev :
forall l, permutation l (rev l).
Proof.
induction l.
simpl; trivial using permut_refl.
simpl.
apply permut_add_cons_inside.
rewrite <- app_nil_end. trivial.
Qed.
(** * Some inversion results. *)
Lemma permut_conv_inv :
forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
Proof.
intros e l1 l2; unfold permutation, meq; simpl; intros H a;
generalize (H a); apply plus_reg_l.
Qed.
Lemma permut_app_inv1 :
forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
Proof.
intros l l1 l2; unfold permutation, meq; simpl;
intros H a; generalize (H a); clear H.
do 2 rewrite list_contents_app.
simpl.
intros; apply plus_reg_l with (multiplicity (list_contents l) a).
rewrite plus_comm; rewrite H; rewrite plus_comm.
trivial.
Qed.
(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
Fact if_eqA_then : forall a a' (B:Type)(b b':B),
eqA a a' -> (if eqA_dec a a' then b else b') = b.
Proof.
intros. destruct eqA_dec as [_|NEQ]; auto.
contradict NEQ; auto.
Qed.
Lemma permut_app_inv2 :
forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
Proof.
intros l l1 l2; unfold permutation, meq; simpl;
intros H a; generalize (H a); clear H.
do 2 rewrite list_contents_app.
simpl.
intros; apply plus_reg_l with (multiplicity (list_contents l) a).
trivial.
Qed.
Lemma permut_remove_hd_eq :
forall l l1 l2 a b, eqA a b ->
permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
Proof.
unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
specialize H with a0.
rewrite list_contents_app in *; simpl in *.
apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
rewrite H; clear H.
symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
rewrite plus_comm.
destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
decide (eqA_dec b a0) with Ha; reflexivity.
Qed.
Lemma permut_remove_hd :
forall l l1 l2 a,
permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
Proof.
eauto using permut_remove_hd_eq, Equivalence_Reflexive.
Qed.
Fact if_eqA_else : forall a a' (B:Type)(b b':B),
~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
Proof.
intros. decide (eqA_dec a a') with H; auto.
Qed.
Fact if_eqA_refl : forall a (B:Type)(b b':B),
(if eqA_dec a a then b else b') = b.
Proof.
intros; apply (decide_left (eqA_dec a a)); auto with *.
Qed.
(** PL: Inutilisable dans un rewrite sans un change prealable. *)
Global Instance if_eqA (B:Type)(b b':B) :
Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
Proof.
intros x x' Hxx' y y' Hyy'.
intros; destruct (eqA_dec x y) as [H|H];
destruct (eqA_dec x' y') as [H'|H']; auto.
contradict H'; transitivity x; auto with *; transitivity y; auto with *.
contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
Qed.
Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1' a2 then b else b').
Proof.
intros; destruct (eqA_dec a1 a2) as [A1|A1];
destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
contradict A1'; transitivity a1; eauto with *.
contradict A1; transitivity a1'; eauto with *.
Qed.
Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
(if eqA_dec a1 a2' then b else b').
Proof.
intros; destruct (eqA_dec a1 a2) as [A2|A2];
destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
contradict A2'; transitivity a2; eauto with *.
contradict A2; transitivity a2'; eauto with *.
Qed.
Global Instance multiplicity_eqA (l:list A) :
Proper (eqA==>@eq _) (multiplicity (list_contents l)).
Proof.
intros x x' Hxx'.
induction l as [|y l Hl]; simpl; auto.
rewrite (@if_eqA_rewrite_r y x x'); auto.
Qed.
Lemma multiplicity_InA :
forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
Proof.
induction l.
simpl.
split; inversion 1.
simpl.
intros a'; split; intros H. inversion_clear H.
apply (decide_left (eqA_dec a a')); auto with *.
destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
Qed.
Lemma multiplicity_InA_O :
forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
Proof.
intros l a; rewrite multiplicity_InA;
destruct (multiplicity (list_contents l) a); auto with arith.
destruct 1; auto with arith.
Qed.
Lemma multiplicity_InA_S :
forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
Proof.
intros l a; rewrite multiplicity_InA; auto with arith.
Qed.
Lemma multiplicity_NoDupA : forall l,
NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
Proof.
induction l.
simpl.
split; auto with arith.
split; simpl.
inversion_clear 1.
rewrite IHl in H1.
intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
rewrite <- EQ.
rewrite multiplicity_InA_O; auto.
intros; constructor.
rewrite multiplicity_InA.
specialize (H a).
rewrite if_eqA_refl in H.
clear IHl; omega.
rewrite IHl; intros.
specialize (H a0). omega.
Qed.
(** Permutation is compatible with InA. *)
Lemma permut_InA_InA :
forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
Proof.
intros l1 l2 e.
do 2 rewrite multiplicity_InA.
unfold permutation, meq.
intros H;rewrite H; auto.
Qed.
Lemma permut_cons_InA :
forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
Proof.
intros; apply (permut_InA_InA (e:=e) H); auto with *.
Qed.
(** Permutation of an empty list. *)
Lemma permut_nil :
forall l, permutation l [] -> l = [].
Proof.
intro l; destruct l as [ | e l ]; trivial.
assert (InA eqA e (e::l)) by (auto with *).
intro Abs; generalize (permut_InA_InA Abs H).
inversion 1.
Qed.
(** Permutation for short lists. *)
Lemma permut_length_1:
forall a b, permutation [a] [b] -> eqA a b.
Proof.
intros a b; unfold permutation, meq.
intro P; specialize (P b); simpl in *.
rewrite if_eqA_refl in *.
destruct (eqA_dec a b); simpl; auto; discriminate.
Qed.
Lemma permut_length_2 :
forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
(eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
Proof.
intros a1 b1 a2 b2 P.
assert (H:=permut_cons_InA P).
inversion_clear H.
left; split; auto.
apply permut_length_1.
red; red; intros.
specialize (P a). simpl in *.
rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
right.
inversion_clear H0; [|inversion H].
split; auto.
apply permut_length_1.
red; red; intros.
specialize (P a); simpl in *.
rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
Qed.
(** Permutation is compatible with length. *)
Lemma permut_length :
forall l1 l2, permutation l1 l2 -> length l1 = length l2.
Proof.
induction l1; intros l2 H.
rewrite (permut_nil (permut_sym H)); auto.
assert (H0:=permut_cons_InA H).
destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
subst l2.
rewrite app_length.
simpl; rewrite <- plus_n_Sm; f_equal.
rewrite <- app_length.
apply IHl1.
apply permut_remove_hd with b.
apply permut_trans with (a::l1); auto.
revert H1; unfold permutation, meq; simpl.
intros; f_equal; auto.
rewrite (@if_eqA_rewrite_l a b a0); auto.
Qed.
Lemma NoDupA_equivlistA_permut :
forall l l', NoDupA eqA l -> NoDupA eqA l' ->
equivlistA eqA l l' -> permutation l l'.
Proof.
intros.
red; unfold meq; intros.
rewrite multiplicity_NoDupA in H, H0.
generalize (H a) (H0 a) (H1 a); clear H H0 H1.
do 2 rewrite multiplicity_InA.
destruct 3; omega.
Qed.
End Permut.
Section Permut_map.
Variables A B : Type.
Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Hypothesis eqA_equiv : Equivalence eqA.
Variable eqB : B->B->Prop.
Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Hypothesis eqB_trans : Transitive eqB.
(** Permutation is compatible with map. *)
Lemma permut_map :
forall f,
(Proper (eqA==>eqB) f) ->
forall l1 l2, permutation _ eqA_dec l1 l2 ->
permutation _ eqB_dec (map f l1) (map f l2).
Proof.
intros f; induction l1.
intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
intros l2 P.
simpl.
assert (H0:=permut_cons_InA eqA_equiv P).
destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
subst l2.
rewrite map_app.
simpl.
apply permut_trans with (f b :: map f l1).
revert H1; unfold permutation, meq; simpl.
intros; f_equal; auto.
destruct (eqB_dec (f b) a0) as [H2|H2];
destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
destruct H3; transitivity (f b); auto with *.
destruct H2; transitivity (f a); auto with *.
apply permut_add_cons_inside.
rewrite <- map_app.
apply IHl1; auto.
apply permut_remove_hd with b; trivial.
apply permut_trans with (a::l1); auto.
revert H1; unfold permutation, meq; simpl.
intros; f_equal; auto.
rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
Qed.
End Permut_map.
Require Import Permutation.
Section Permut_permut.
Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Hypothesis eqA_equiv : Equivalence eqA.
Lemma Permutation_impl_permutation : forall l l',
Permutation l l' -> permutation _ eqA_dec l l'.
Proof.
induction 1.
apply permut_refl.
apply permut_cons; auto using Equivalence_Reflexive.
change (x :: y :: l) with ([x] ++ y :: l);
apply permut_add_cons_inside; simpl;
apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
apply permut_trans with l'; trivial.
Qed.
Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
Proof.
induction 1.
apply permut_refl.
apply permut_cons_eq; trivial.
Qed.
Lemma permutation_Permutation : forall l l',
permutation _ eqA_dec l l' <->
exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
Proof.
split; intro H.
(* -> *)
induction l in l', H |- *.
exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
pose proof H as H'.
apply permut_cons_InA, InA_split in H
as (l1 & y & l2 & Heq & ->); trivial.
apply permut_remove_hd_eq, IHl in H'
as (l'' & IHP & IHA); clear IHl; trivial.
apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
exists (l1'' ++ a :: l2''); split.
apply Permutation_cons_app; trivial.
apply Forall2_app, Forall2_cons; trivial.
(* <- *)
destruct H as (l'' & H & Heq).
apply permut_trans with l''.
apply Permutation_impl_permutation; trivial.
apply permut_eqA; trivial.
Qed.
End Permut_permut.
(* begin hide *)
(** For compatibilty *)
Notation permut_right := permut_cons (only parsing).
Notation permut_tran := permut_trans (only parsing).
(* end hide *)

632
samples/Coq/Permutation.v
View File

@@ -1,632 +0,0 @@
(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
Laurent Thery (Huffmann contribution, October 2003) *)
Require Import List Setoid Compare_dec Morphisms.
Import ListNotations. (* For notations [] and [a;b;c] *)
Set Implicit Arguments.
Section Permutation.
Variable A:Type.
Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
Permutation l l' -> Permutation l' l'' -> Permutation l l''.
Local Hint Constructors Permutation.
(** Some facts about [Permutation] *)
Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
Proof.
intros l HF.
remember (@nil A) as m in HF.
induction HF; discriminate || auto.
Qed.
Theorem Permutation_nil_cons : forall (l : list A) (x : A),
~ Permutation nil (x::l).
Proof.
intros l x HF.
apply Permutation_nil in HF; discriminate.
Qed.
(** Permutation over lists is a equivalence relation *)
Theorem Permutation_refl : forall l : list A, Permutation l l.
Proof.
induction l; constructor. exact IHl.
Qed.
Theorem Permutation_sym : forall l l' : list A,
Permutation l l' -> Permutation l' l.
Proof.
intros l l' Hperm; induction Hperm; auto.
apply perm_trans with (l':=l'); assumption.
Qed.
Theorem Permutation_trans : forall l l' l'' : list A,
Permutation l l' -> Permutation l' l'' -> Permutation l l''.
Proof.
exact perm_trans.
Qed.
End Permutation.
Hint Resolve Permutation_refl perm_nil perm_skip.
(* These hints do not reduce the size of the problem to solve and they
must be used with care to avoid combinatoric explosions *)
Local Hint Resolve perm_swap perm_trans.
Local Hint Resolve Permutation_sym Permutation_trans.
(* This provides reflexivity, symmetry and transitivity and rewriting
on morphims to come *)
Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
Equivalence_Reflexive := @Permutation_refl A ;
Equivalence_Symmetric := @Permutation_sym A ;
Equivalence_Transitive := @Permutation_trans A }.
Instance Permutation_cons A :
Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
Proof.
repeat intro; subst; auto using perm_skip.
Qed.
Section Permutation_properties.
Variable A:Type.
Implicit Types a b : A.
Implicit Types l m : list A.
(** Compatibility with others operations on lists *)
Theorem Permutation_in : forall (l l' : list A) (x : A),
Permutation l l' -> In x l -> In x l'.
Proof.
intros l l' x Hperm; induction Hperm; simpl; tauto.
Qed.
Global Instance Permutation_in' :
Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
Proof.
repeat red; intros; subst; eauto using Permutation_in.
Qed.
Lemma Permutation_app_tail : forall (l l' tl : list A),
Permutation l l' -> Permutation (l++tl) (l'++tl).
Proof.
intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
eapply Permutation_trans with (l':=l'++tl); trivial.
Qed.
Lemma Permutation_app_head : forall (l tl tl' : list A),
Permutation tl tl' -> Permutation (l++tl) (l++tl').
Proof.
intros l tl tl' Hperm; induction l;
[trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
Qed.
Theorem Permutation_app : forall (l m l' m' : list A),
Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
Proof.
intros l m l' m' Hpermll' Hpermmm';
induction Hpermll' as [|x l l'|x y l|l l' l''];
repeat rewrite <- app_comm_cons; auto.
apply Permutation_trans with (l' := (x :: y :: l ++ m));
[idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
apply Permutation_trans with (l' := (l' ++ m')); try assumption.
apply Permutation_app_tail; assumption.
Qed.
Global Instance Permutation_app' :
Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
Proof.
repeat intro; now apply Permutation_app.
Qed.
Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
Permutation l l' -> Permutation tl tl' ->
Permutation (l ++ a :: tl) (l' ++ a :: tl').
Proof.
intros; apply Permutation_app; auto.
Qed.
Lemma Permutation_cons_append : forall (l : list A) x,
Permutation (x :: l) (l ++ x :: nil).
Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
Local Hint Resolve Permutation_cons_append.
Theorem Permutation_app_comm : forall (l l' : list A),
Permutation (l ++ l') (l' ++ l).
Proof.
induction l as [|x l]; simpl; intro l'.
rewrite app_nil_r; trivial. rewrite IHl.
rewrite app_comm_cons, Permutation_cons_append.
now rewrite <- app_assoc.
Qed.
Local Hint Resolve Permutation_app_comm.
Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
Proof.
intros l l1 l2 a H. rewrite H.
rewrite app_comm_cons, Permutation_cons_append.
now rewrite <- app_assoc.
Qed.
Local Hint Resolve Permutation_cons_app.
Theorem Permutation_middle : forall (l1 l2:list A) a,
Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
Proof.
auto.
Qed.
Local Hint Resolve Permutation_middle.
Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
Proof.
induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
Qed.
Global Instance Permutation_rev' :
Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
Proof.
repeat intro; now rewrite <- 2 Permutation_rev.
Qed.
Theorem Permutation_length : forall (l l' : list A),
Permutation l l' -> length l = length l'.
Proof.
intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
Qed.
Global Instance Permutation_length' :
Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
Proof.
exact Permutation_length.
Qed.
Theorem Permutation_ind_bis :
forall P : list A -> list A -> Prop,
P [] [] ->
(forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
(forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
(forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
forall l l', Permutation l l' -> P l l'.
Proof.
intros P Hnil Hskip Hswap Htrans.
induction 1; auto.
apply Htrans with (x::y::l); auto.
apply Hswap; auto.
induction l; auto.
apply Hskip; auto.
apply Hskip; auto.
induction l; auto.
eauto.
Qed.
Ltac break_list l x l' H :=
destruct l as [|x l']; simpl in *;
injection H; intros; subst; clear H.
Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
~ Permutation nil (l++x::l').
Proof.
intros l l' x HF.
apply Permutation_nil in HF. destruct l; discriminate.
Qed.
Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
Proof.
intros l1 l2 l3 l4 a; revert l1 l2 l3 l4.
set (P l l' :=
forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 ->
Permutation (l1++l2) (l3++l4)).
cut (forall l l', Permutation l l' -> P l l').
intros H; intros; eapply H; eauto.
apply (Permutation_ind_bis P); unfold P; clear P.
- (* nil *)
intros; now destruct l1.
- (* skip *)
intros x l l' H IH; intros.
break_list l1 b l1' H0; break_list l3 c l3' H1.
auto.
now rewrite H.
now rewrite <- H.
now rewrite (IH _ _ _ _ eq_refl eq_refl).
- (* swap *)
intros x y l l' Hp IH; intros.
break_list l1 b l1' H; break_list l3 c l3' H0.
auto.
break_list l3' b l3'' H.
auto.
constructor. now rewrite Permutation_middle.
break_list l1' c l1'' H1.
auto.
constructor. now rewrite Permutation_middle.
break_list l3' d l3'' H; break_list l1' e l1'' H1.
auto.
rewrite perm_swap. constructor. now rewrite Permutation_middle.
rewrite perm_swap. constructor. now rewrite Permutation_middle.
now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl).
- (*trans*)
intros.
destruct (In_split a l') as (l'1,(l'2,H6)).
rewrite <- H.
subst l.
apply in_or_app; right; red; auto.
apply perm_trans with (l'1++l'2).
apply (H0 _ _ _ _ H3 H6).
apply (H2 _ _ _ _ H6 H4).
Qed.
Theorem Permutation_cons_inv l l' a :
Permutation (a::l) (a::l') -> Permutation l l'.
Proof.
intro H; exact (Permutation_app_inv [] l [] l' a H).
Qed.
Theorem Permutation_cons_app_inv l l1 l2 a :
Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
Proof.
intro H; exact (Permutation_app_inv [] l l1 l2 a H).
Qed.
Theorem Permutation_app_inv_l : forall l l1 l2,
Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
Proof.
induction l; simpl; auto.
intros.
apply IHl.
apply Permutation_cons_inv with a; auto.
Qed.
Theorem Permutation_app_inv_r : forall l l1 l2,
Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
Proof.
induction l.
intros l1 l2; do 2 rewrite app_nil_r; auto.
intros.
apply IHl.
apply Permutation_app_inv with a; auto.
Qed.
Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
Proof.
intros a l H; remember [a] as m in H.
induction H; try (injection Heqm as -> ->; clear Heqm);
discriminate || auto.
apply Permutation_nil in H as ->; trivial.
Qed.
Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
Proof.
intros a b H.
apply Permutation_length_1_inv in H; injection H as ->; trivial.
Qed.
Lemma Permutation_length_2_inv :
forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
Proof.
intros a1 a2 l H; remember [a1;a2] as m in H.
revert a1 a2 Heqm.
induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
discriminate || (try tauto).
apply Permutation_length_1_inv in H as ->; left; auto.
apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
auto.
Qed.
Lemma Permutation_length_2 :
forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
Proof.
intros a1 b1 a2 b2 H.
apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
Qed.
Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 ->
forall x, In x l <-> a = x \/ In x (l1++l2).
Proof.
intros; subst; rewrite !in_app_iff; simpl. tauto.
Qed.
Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' ->
length l = length l' -> incl l l' -> incl l' l.
Proof.
intros N. revert l'. induction N as [|a l Hal Hl IH].
- destruct l'; now auto.
- intros l' Hl' E H x Hx.
assert (Ha : In a l') by (apply H; simpl; auto).
destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha.
rewrite in_middle in Hx; eauto.
destruct Hx as [Hx|Hx]; [left|right]; auto.
apply (IH (l1++l2)); auto.
* apply NoDup_remove_1 with a; rewrite <- H12; auto.
* apply eq_add_S.
simpl in E; rewrite E, H12, !app_length; simpl; auto with arith.
* intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto).
rewrite in_middle in Hy'; eauto.
destruct Hy'; auto. subst y; intuition.
Qed.
Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
(forall x:A, In x l <-> In x l') -> Permutation l l'.
Proof.
intros N. revert l'. induction N as [|a l Hal Hl IH].
- destruct l'; simpl; auto.
intros Hl' H. exfalso. rewrite (H a); auto.
- intros l' Hl' H.
assert (Ha : In a l') by (apply H; simpl; auto).
destruct (In_split _ _ Ha) as (l1 & l2 & H12).
rewrite H12.
apply Permutation_cons_app.
apply IH; auto.
* apply NoDup_remove_1 with a; rewrite <- H12; auto.
* intro x. split; intros Hx.
+ assert (Hx' : In x l') by (apply H; simpl; auto).
rewrite in_middle in Hx'; eauto.
destruct Hx'; auto. subst; intuition.
+ assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto).
rewrite <- H in Hx'. destruct Hx'; auto.
subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx).
Qed.
Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
length l = length l' -> incl l l' -> Permutation l l'.
Proof.
intros. apply NoDup_Permutation; auto.
split; auto. apply NoDup_cardinal_incl; auto.
Qed.
Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
Proof.
induction 1; auto.
* inversion_clear 1; constructor; eauto using Permutation_in.
* inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *.
constructor. simpl; intuition. constructor; intuition.
Qed.
Global Instance Permutation_NoDup' :
Proper (@Permutation A ==> iff) (@NoDup A) | 10.
Proof.
repeat red; eauto using Permutation_NoDup.
Qed.
End Permutation_properties.
Section Permutation_map.
Variable A B : Type.
Variable f : A -> B.
Lemma Permutation_map l l' :
Permutation l l' -> Permutation (map f l) (map f l').
Proof.
induction 1; simpl; eauto.
Qed.
Global Instance Permutation_map' :
Proper (@Permutation A ==> @Permutation B) (map f) | 10.
Proof.
exact Permutation_map.
Qed.
End Permutation_map.
Section Injection.
Definition injective {A B} (f : A->B) :=
forall x y, f x = f y -> x = y.
Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) :
injective f -> NoDup l -> NoDup (map f l).
Proof.
intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial.
rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst.
Qed.
Lemma injective_bounded_surjective n f :
injective f ->
(forall x, x < n -> f x < n) ->
(forall y, y < n -> exists x, x < n /\ f x = y).
Proof.
intros Hf H.
set (l := seq 0 n).
assert (P : incl (map f l) l).
{ intros x. rewrite in_map_iff. intros (y & <- & Hy').
unfold l in *. rewrite in_seq in *. simpl in *.
destruct Hy' as (_,Hy'). auto with arith. }
assert (P' : incl l (map f l)).
{ unfold l.
apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup.
now rewrite map_length. }
intros x Hx.
assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith).
apply P' in Hx'.
rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy').
exists y; split; auto. unfold l in *; rewrite in_seq in Hy'.
destruct Hy'; auto with arith.
Qed.
Lemma nat_bijection_Permutation n f :
injective f -> (forall x, x < n -> f x < n) ->
let l := seq 0 n in Permutation (map f l) l.
Proof.
intros Hf BD.
apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup.
* now rewrite map_length.
* intros x. rewrite in_map_iff. intros (y & <- & Hy').
rewrite in_seq in *. simpl in *.
destruct Hy' as (_,Hy'). auto with arith.
Qed.
End Injection.
Section Permutation_alt.
Variable A:Type.
Implicit Type a : A.
Implicit Type l : list A.
(** Alternative characterization of permutation
via [nth_error] and [nth] *)
Let adapt f n :=
let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
Let adapt_injective f : injective f -> injective (adapt f).
Proof.
unfold adapt. intros Hf x y EQ.
destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].
- now apply eq_add_S, Hf.
- apply Lt.le_lt_or_eq in LE.
destruct LE as [LT|EQ']; [|now apply Hf in EQ'].
unfold lt in LT. rewrite EQ in LT.
rewrite <- (Lt.S_pred _ _ LT') in LT.
elim (Lt.lt_not_le _ _ LT' LT).
- apply Lt.le_lt_or_eq in LE'.
destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].
unfold lt in LT'. rewrite <- EQ in LT'.
rewrite <- (Lt.S_pred _ _ LT) in LT'.
elim (Lt.lt_not_le _ _ LT LT').
- apply eq_add_S, Hf.
now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
Qed.
Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 ->
forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
Proof.
unfold adapt. intros Hf E n.
destruct le_lt_dec as [LE|LT].
- apply Lt.le_lt_or_eq in LE.
destruct LE as [LT|EQ]; [|now apply Hf in EQ].
rewrite <- E in LT.
rewrite 2 nth_error_app1; auto.
- rewrite (Lt.S_pred _ _ LT) at 1.
rewrite <- E, (Lt.S_pred _ _ LT) in LT.
rewrite 2 nth_error_app2; auto with arith.
rewrite <- Minus.minus_Sn_m; auto with arith.
Qed.
Lemma Permutation_nth_error l l' :
Permutation l l' <->
(length l = length l' /\
exists f:nat->nat,
injective f /\ forall n, nth_error l' n = nth_error l (f n)).
Proof.
split.
{ intros P.
split; [now apply Permutation_length|].
induction P.
- exists (fun n => n).
split; try red; auto.
- destruct IHP as (f & Hf & Hf').
exists (fun n => match n with O => O | S n => S (f n) end).
split; try red.
* intros [|y] [|z]; simpl; now auto.
* intros [|n]; simpl; auto.
- exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).
split; try red.
* intros [|[|z]] [|[|t]]; simpl; now auto.
* intros [|[|n]]; simpl; auto.
- destruct IHP1 as (f & Hf & Hf').
destruct IHP2 as (g & Hg & Hg').
exists (fun n => f (g n)).
split; try red.
* auto.
* intros n. rewrite <- Hf'; auto. }
{ revert l. induction l'.
- intros [|l] (E & _); now auto.
- intros l (E & f & Hf & Hf').
simpl in E.
assert (Ha : nth_error l (f 0) = Some a)
by (symmetry; apply (Hf' 0)).
destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).
rewrite L12. rewrite <- Permutation_middle. constructor.
apply IHl'; split; [|exists (adapt f); split].
* revert E. rewrite L12, !app_length. simpl.
rewrite <- plus_n_Sm. now injection 1.
* now apply adapt_injective.
* intro n. rewrite <- (adapt_ok a), <- L12; auto.
apply (Hf' (S n)). }
Qed.
Lemma Permutation_nth_error_bis l l' :
Permutation l l' <->
exists f:nat->nat,
injective f /\
(forall n, n < length l -> f n < length l) /\
(forall n, nth_error l' n = nth_error l (f n)).
Proof.
rewrite Permutation_nth_error; split.
- intros (E & f & Hf & Hf').
exists f. do 2 (split; trivial).
intros n Hn.
destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.
rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.
elim (Lt.lt_not_le _ _ Hn LE).
- intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].
assert (H : length l' <= length l') by auto with arith.
rewrite <- nth_error_None, Hf3, nth_error_None in H.
destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
[|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].
apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial.
rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.
destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy').
apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy).
Qed.
Lemma Permutation_nth l l' d :
Permutation l l' <->
(let n := length l in
length l' = n /\
exists f:nat->nat,
(forall x, x < n -> f x < n) /\
(forall x y, x < n -> y < n -> f x = f y -> x = y) /\
(forall x, x < n -> nth x l' d = nth (f x) l d)).
Proof.
split.
- intros H.
assert (E := Permutation_length H).
split; auto.
apply Permutation_nth_error_bis in H.
destruct H as (f & Hf & Hf2 & Hf3).
exists f. split; [|split]; auto.
intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default.
now rewrite Hf3.
- intros (E & f & Hf1 & Hf2 & Hf3).
rewrite Permutation_nth_error.
split; auto.
exists (fun n => if le_lt_dec (length l) n then n else f n).
split.
* intros x y.
destruct le_lt_dec as [LE|LT];
destruct le_lt_dec as [LE'|LT']; auto.
+ apply Hf1 in LT'. intros ->.
elim (Lt.lt_irrefl (f y)). eapply Lt.lt_le_trans; eauto.
+ apply Hf1 in LT. intros <-.
elim (Lt.lt_irrefl (f x)). eapply Lt.lt_le_trans; eauto.
* intros n.
destruct le_lt_dec as [LE|LT].
+ assert (LE' : length l' <= n) by (now rewrite E).
rewrite <- nth_error_None in LE, LE'. congruence.
+ assert (LT' : n < length l') by (now rewrite E).
specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3.
unfold nth_default in Hf3.
apply Hf1 in LT.
rewrite <- nth_error_Some in LT, LT'.
do 2 destruct nth_error; congruence.
Qed.
End Permutation_alt.
(* begin hide *)
Notation Permutation_app_swap := Permutation_app_comm (only parsing).
(* end hide *)

2
samples/Coq/Sorting.v
View File

@@ -1,2 +0,0 @@
Require Export Sorted.
Require Export Mergesort.

419
samples/Coq/interval_discr.v
View File

@@ -1,419 +0,0 @@
(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m
- preliminary results on the irrelevance of boundedness proofs
- introduce the notion of finite cardinal |A|
- prove that |{p:nat|p<=n}| = n
- prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A
- prove that equality is decidable on A
- conclude
*)
(** * Preliminary results on [nat] and [le] *)
(** Proving axiom K on [nat] *)
Require Import Eqdep_dec.
Require Import Arith.
Theorem eq_rect_eq_nat :
forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
Proof.
intros.
apply K_dec_set with (p := h).
apply eq_nat_dec.
reflexivity.
Qed.
(** Proving unicity of proofs of [(n<=m)%nat] *)
Scheme le_ind' := Induction for le Sort Prop.
Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
Proof.
induction p using le_ind'; intro q.
replace (le_n n) with
(eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
2:reflexivity.
generalize (refl_equal n).
pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
rewrite <- eq_rect_eq_nat; trivial.
contradiction (le_Sn_n m); rewrite <- e; assumption.
replace (le_S n m p) with
(eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
2:reflexivity.
generalize (refl_equal (S m)).
pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
contradiction (le_Sn_n m); rewrite Heq; assumption.
injection HeqS; intro Heq; generalize l HeqS.
rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
rewrite (IHp l0); reflexivity.
Qed.
(** Proving irrelevance of boundedness proofs while building
elements of interval *)
Lemma dep_pair_intro :
forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y ->
exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy.
Proof.
intros n x y Hx Hy Heq.
generalize Hy.
rewrite <- Heq.
intros.
rewrite (le_uniqueness_proof x n Hx Hy0).
reflexivity.
Qed.
(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *)
(** Definition of having finite cardinality [n+1] for a set [A] *)
Definition card (A:Set) n :=
exists f,
(forall x:A, f x <= n) /\
(forall x y:A, f x = f y -> x = y) /\
(forall m, m <= n -> exists x:A, f x = m).
Require Import Arith.
(** Showing that the interval [0;n] has cardinality [n+1] *)
Theorem card_interval : forall n, card {x:nat|x<=n} n.
Proof.
intro n.
exists (fun x:{x:nat|x<=n} => proj1_sig x).
split.
(* bounded *)
intro x; apply (proj2_sig x).
split.
(* injectivity *)
intros (p,Hp) (q,Hq).
simpl.
intro Hpq.
apply dep_pair_intro; assumption.
(* surjectivity *)
intros m Hmn.
exists (exist (fun x : nat => x <= n) m Hmn).
reflexivity.
Qed.
(** Showing that equality on the interval [0;n] is decidable *)
Lemma interval_dec :
forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}.
Proof.
intros n (p,Hp).
induction p; intros ([|q],Hq).
left.
apply dep_pair_intro.
reflexivity.
right.
intro H; discriminate H.
right.
intro H; discriminate H.
assert (Hp' : p <= n).
apply le_Sn_le; assumption.
assert (Hq' : q <= n).
apply le_Sn_le; assumption.
destruct (IHp Hp' (exist (fun m => m <= n) q Hq'))
as [Heq|Hneq].
left.
injection Heq; intro Heq'.
apply dep_pair_intro.
apply eq_S.
assumption.
right.
intro HeqS.
injection HeqS; intro Heq.
apply Hneq.
apply dep_pair_intro.
assumption.
Qed.
(** Showing that the cardinality relation is functional on decidable sets *)
Lemma card_inj_aux :
forall (A:Type) f g n,
(forall x:A, f x <= 0) ->
(forall x y:A, f x = f y -> x = y) ->
(forall m, m <= S n -> exists x:A, g x = m)
-> False.
Proof.
intros A f g n Hfbound Hfinj Hgsurj.
destruct (Hgsurj (S n) (le_n _)) as (x,Hx).
destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx').
assert (Hfx : 0 = f x).
apply le_n_O_eq.
apply Hfbound.
assert (Hfx' : 0 = f x').
apply le_n_O_eq.
apply Hfbound.
assert (x=x').
apply Hfinj.
rewrite <- Hfx.
rewrite <- Hfx'.
reflexivity.
rewrite H in Hx.
rewrite Hx' in Hx.
apply (n_Sn _ Hx).
Qed.
(** For [dec_restrict], we use a lemma on the negation of equality
that requires proof-irrelevance. It should be possible to avoid this
lemma by generalizing over a first-order definition of [x<>y], say
[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such
[neq], unicity of proofs could be proven *)
Require Import Classical.
Lemma neq_dep_intro :
forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y ->
exist (fun x => x <> z) x p = exist (fun x => x <> z) y q.
Proof.
intros A z x y p q Heq.
generalize q; clear q; rewrite <- Heq; intro q.
rewrite (proof_irrelevance _ p q); reflexivity.
Qed.
Lemma dec_restrict :
forall (A:Set),
(forall x y :A, {x=y}+{x<>y}) ->
forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}.
Proof.
intros A Hdec z (x,Hx) (y,Hy).
destruct (Hdec x y) as [Heq|Hneq].
left; apply neq_dep_intro; assumption.
right; intro Heq; injection Heq; exact Hneq.
Qed.
Lemma pred_inj : forall n m,
0 <> n -> 0 <> m -> pred m = pred n -> m = n.
Proof.
destruct n.
intros m H; destruct H; reflexivity.
destruct m.
intros _ H; destruct H; reflexivity.
simpl; intros _ _ H.
rewrite H.
reflexivity.
Qed.
Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m.
Proof.
intros n m Hle Hneq.
destruct (le_lt_eq_dec n m Hle).
assumption.
contradiction.
Qed.
Lemma inj_restrict :
forall (A:Set) (f:A->nat) x y z,
(forall x y : A, f x = f y -> x = y)
-> x <> z -> f y < f z -> f z <= f x
-> pred (f x) = f y
-> False.
(* Search error sans le type de f !! *)
Proof.
intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
assert (f z <> f x).
apply sym_not_eq.
intro Heqf.
apply Hneqx.
apply Hfinj.
assumption.
assert (f x = S (f y)).
assert (0 < f x).
apply le_lt_trans with (f z).
apply le_O_n.
apply le_neq_lt; assumption.
apply pred_inj.
apply O_S.
apply lt_O_neq; assumption.
exact Heq.
assert (f z <= f y).
destruct (le_lt_or_eq _ _ Hfx).
apply lt_n_Sm_le.
rewrite <- H0.
assumption.
contradiction Hneqx.
symmetry.
apply Hfinj.
assumption.
contradiction (lt_not_le (f y) (f z)).
Qed.
Theorem card_inj : forall m n (A:Set),
(forall x y :A, {x=y}+{x<>y}) ->
card A m -> card A n -> m = n.
Proof.
induction m; destruct n;
intros A Hdec
(f,(Hfbound,(Hfinj,Hfsurj)))
(g,(Hgbound,(Hginj,Hgsurj))).
(* 0/0 *)
reflexivity.
(* 0/Sm *)
destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj).
(* Sn/0 *)
destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj).
(* Sn/Sm *)
destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx).
rewrite IHm with (n:=n) (A := {x:A|x<>xSn}).
reflexivity.
(* decidability of eq on {x:A|x<>xSm} *)
apply dec_restrict.
assumption.
(* cardinality of {x:A|x<>xSn} is m *)
pose (f' := fun x' : {x:A|x<>xSn} =>
let (x,Hneq) := x' in
if le_lt_dec (f xSn) (f x)
then pred (f x)
else f x).
exists f'.
split.
(* f' is bounded *)
unfold f'.
intros (x,_).
destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge].
change m with (pred (S m)).
apply le_pred.
apply Hfbound.
apply le_S_n.
apply le_trans with (f xSn).
exact Hge.
apply Hfbound.
split.
(* f' is injective *)
unfold f'.
intros (x,Hneqx) (y,Hneqy) Heqf'.
destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx];
destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
(* f xSn <= f x et f xSn <= f y *)
assert (Heq : x = y).
apply Hfinj.
assert (f xSn <> f y).
apply sym_not_eq.
intro Heqf.
apply Hneqy.
apply Hfinj.
assumption.
assert (0 < f y).
apply le_lt_trans with (f xSn).
apply le_O_n.
apply le_neq_lt; assumption.
assert (f xSn <> f x).
apply sym_not_eq.
intro Heqf.
apply Hneqx.
apply Hfinj.
assumption.
assert (0 < f x).
apply le_lt_trans with (f xSn).
apply le_O_n.
apply le_neq_lt; assumption.
apply pred_inj.
apply lt_O_neq; assumption.
apply lt_O_neq; assumption.
assumption.
apply neq_dep_intro; assumption.
(* f y < f xSn <= f x *)
destruct (inj_restrict A f x y xSn); assumption.
(* f x < f xSn <= f y *)
symmetry in Heqf'.
destruct (inj_restrict A f y x xSn); assumption.
(* f x < f xSn et f y < f xSn *)
assert (Heq : x=y).
apply Hfinj; assumption.
apply neq_dep_intro; assumption.
(* f' is surjective *)
intros p Hlep.
destruct (le_lt_dec (f xSn) p) as [Hle|Hlt].
(* case f xSn <= p *)
destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx).
assert (Hneq : x <> xSn).
intro Heqx.
rewrite Heqx in Hx.
rewrite Hx in Hle.
apply le_Sn_n with p; assumption.
exists (exist (fun a => a<>xSn) x Hneq).
unfold f'.
destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
rewrite Hx; reflexivity.
rewrite Hx in Hlt'.
contradiction (le_not_lt (f xSn) p).
apply lt_trans with (S p).
apply lt_n_Sn.
assumption.
(* case p < f xSn *)
destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx).
assert (Hneq : x <> xSn).
intro Heqx.
rewrite Heqx in Hx.
rewrite Hx in Hlt.
apply (lt_irrefl p).
assumption.
exists (exist (fun a => a<>xSn) x Hneq).
unfold f'.
destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
rewrite Hx in Hle'.
contradiction (lt_irrefl p).
apply lt_le_trans with (f xSn); assumption.
assumption.
(* cardinality of {x:A|x<>xSn} is n *)
pose (g' := fun x' : {x:A|x<>xSn} =>
let (x,Hneq) := x' in
if Hdec x xSn then 0 else g x).
exists g'.
split.
(* g is bounded *)
unfold g'.
intros (x,_).
destruct (Hdec x xSn) as [_|Hneq].
apply le_O_n.
assert (Hle_gx:=Hgbound x).
destruct (le_lt_or_eq _ _ Hle_gx).
apply lt_n_Sm_le.
assumption.
contradiction Hneq.
apply Hginj.
rewrite HSnx.
assumption.
split.
(* g is injective *)
unfold g'.
intros (x,Hneqx) (y,Hneqy) Heqg'.
destruct (Hdec x xSn) as [Heqx|_].
contradiction Hneqx.
destruct (Hdec y xSn) as [Heqy|_].
contradiction Hneqy.
assert (Heq : x=y).
apply Hginj; assumption.
apply neq_dep_intro; assumption.
(* g is surjective *)
intros p Hlep.
destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx).
assert (Hneq : x<>xSn).
intro Heq.
rewrite Heq in Hx.
rewrite Hx in HSnx.
rewrite HSnx in Hlep.
contradiction (le_Sn_n _ Hlep).
exists (exist (fun a => a<>xSn) x Hneq).
simpl.
destruct (Hdec x xSn) as [Heqx|_].
contradiction Hneq.
assumption.
Qed.
(** Conclusion *)
Theorem interval_discr :
forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m.
Proof.
intros n m Heq.
apply card_inj with (A := {p:nat|p<=n}).
apply interval_dec.
apply card_interval.
rewrite Heq.
apply card_interval.
Qed.