mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 09:40:21 +00:00
Merge pull request #3314 from github/coq-kiq
Replace GPL-licensed Coq samples
This commit is contained in:
Arfon Smith
GitHub
@@ -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.
|
||||
85
samples/Coq/Computation.v
Normal file
85
samples/Coq/Computation.v
Normal file
@@ -0,0 +1,85 @@
|
||||
(** The definition of computations, used to represent interactive programs. *)
|
||||
Require Import Coq.NArith.NArith.
|
||||
Require Import ListString.All.
|
||||
|
||||
Local Open Scope type.
|
||||
|
||||
(** System calls. *)
|
||||
Module Command.
|
||||
Inductive t :=
|
||||
| AskCard
|
||||
| AskPIN
|
||||
| CheckPIN (pin : N)
|
||||
| AskAmount
|
||||
| CheckAmount (amount : N)
|
||||
| GiveCard
|
||||
| GiveAmount (amount : N)
|
||||
| ShowError (message : LString.t).
|
||||
|
||||
(** The type of an answer for a command depends on the value of the command. *)
|
||||
Definition answer (command : t) : Type :=
|
||||
match command with
|
||||
| AskCard => bool (* If the given card seems valid. *)
|
||||
| AskPIN => option N (* A number or cancellation. *)
|
||||
| CheckPIN _ => bool (* If the PIN number is valid. *)
|
||||
| AskAmount => option N (* A number or cancellation. *)
|
||||
| CheckAmount _ => bool (* If the amount can be withdrawn. *)
|
||||
| GiveCard => bool (* If the card was given. *)
|
||||
| GiveAmount _ => bool (* If the money was given. *)
|
||||
| ShowError _ => unit (* Show an error message. *)
|
||||
end.
|
||||
End Command.
|
||||
|
||||
(** Computations with I/Os. *)
|
||||
Module C.
|
||||
(** A computation can either does nothing, or do a system call and wait
|
||||
for the answer to run another computation. *)
|
||||
Inductive t : Type :=
|
||||
| Ret : t
|
||||
| Call : forall (command : Command.t), (Command.answer command -> t) -> t.
|
||||
Arguments Ret.
|
||||
Arguments Call _ _.
|
||||
|
||||
(** Some optional notations. *)
|
||||
Module Notations.
|
||||
(** A nicer notation for `Ret`. *)
|
||||
Definition ret : t :=
|
||||
Ret.
|
||||
|
||||
(** We define an explicit apply function so that Coq does not try to expand
|
||||
the notations everywhere. *)
|
||||
Definition apply {A B} (f : A -> B) (x : A) := f x.
|
||||
|
||||
(** System call. *)
|
||||
Notation "'call!' answer ':=' command 'in' X" :=
|
||||
(Call command (fun answer => X))
|
||||
(at level 200, answer ident, command at level 100, X at level 200).
|
||||
|
||||
(** System call with typed answer. *)
|
||||
Notation "'call!' answer : A ':=' command 'in' X" :=
|
||||
(Call command (fun (answer : A) => X))
|
||||
(at level 200, answer ident, command at level 100, A at level 200, X at level 200).
|
||||
|
||||
(** System call ignoring the answer. *)
|
||||
Notation "'do_call!' command 'in' X" :=
|
||||
(Call command (fun _ => X))
|
||||
(at level 200, command at level 100, X at level 200).
|
||||
|
||||
(** This notation is useful to compose computations which wait for a
|
||||
continuation. We do not have an explicit bind operator to simplify the
|
||||
language and the proofs. *)
|
||||
Notation "'let!' x ':=' X 'in' Y" :=
|
||||
(apply X (fun x => Y))
|
||||
(at level 200, x ident, X at level 100, Y at level 200).
|
||||
|
||||
(** Let with a typed answer. *)
|
||||
Notation "'let!' x : A ':=' X 'in' Y" :=
|
||||
(apply X (fun (x : A) => Y))
|
||||
(at level 200, x ident, X at level 100, A at level 200, Y at level 200).
|
||||
|
||||
(** Let ignoring the answer. *)
|
||||
Notation "'do!' X 'in' Y" :=
|
||||
(apply X (fun _ => Y))
|
||||
(at level 200, X at level 100, Y at level 200).
|
||||
End Notations.
|
||||
End C.
|
||||
@@ -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.
|
||||
5944
samples/Coq/JsCorrectness.v
Normal file
5944
samples/Coq/JsCorrectness.v
Normal file
File diff suppressed because it is too large
Load Diff
249
samples/Coq/JsInterpreterExtraction.v
Normal file
249
samples/Coq/JsInterpreterExtraction.v
Normal file
@@ -0,0 +1,249 @@
|
||||
Set Implicit Arguments.
|
||||
Require Import JsSyntax JsInterpreterMonads JsInterpreter JsInit.
|
||||
Require Import LibFix LibList.
|
||||
|
||||
Require Export Shared.
|
||||
Require Export LibTactics LibLogic LibReflect LibList
|
||||
LibOperation LibStruct LibNat LibEpsilon LibFunc LibHeap.
|
||||
Require Flocq.Appli.Fappli_IEEE Flocq.Appli.Fappli_IEEE_bits.
|
||||
|
||||
|
||||
|
||||
(* Here stands some commands to extract relatively correctly the interpreter to Ocaml. *)
|
||||
Extraction Language Ocaml.
|
||||
|
||||
Require Import ExtrOcamlBasic.
|
||||
Require Import ExtrOcamlNatInt.
|
||||
Require Import ExtrOcamlString.
|
||||
|
||||
(* Optimal fixpoint. *)
|
||||
Extraction Inline FixFun3 FixFun3Mod FixFun4 FixFun4Mod FixFunMod curry3 uncurry3 curry4 uncurry4.
|
||||
(* As classical logic statements are now unused, they should not be extracted
|
||||
(otherwise, useless errors will be launched). *)
|
||||
Extraction Inline epsilon epsilon_def classicT arbitrary indefinite_description Inhab_witness Fix isTrue.
|
||||
|
||||
(**************************************************************)
|
||||
(** ** Numerical values *)
|
||||
|
||||
(* number *)
|
||||
|
||||
Extract Inductive positive => float
|
||||
[ "(fun p -> 1. +. (2. *. p))"
|
||||
"(fun p -> 2. *. p)"
|
||||
"1." ]
|
||||
"(fun f2p1 f2p f1 p ->
|
||||
if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))".
|
||||
|
||||
Extract Inductive Z => float [ "0." "" "(~-.)" ]
|
||||
"(fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))".
|
||||
|
||||
Extract Inductive N => float [ "0." "" ]
|
||||
"(fun f0 fp n -> if n=0. then f0 () else fp n)".
|
||||
|
||||
Extract Constant Z.add => "(+.)".
|
||||
Extract Constant Z.succ => "(+.) 1.".
|
||||
Extract Constant Z.pred => "(fun x -> x -. 1.)".
|
||||
Extract Constant Z.sub => "(-.)".
|
||||
Extract Constant Z.mul => "( *. )".
|
||||
Extract Constant Z.opp => "(~-.)".
|
||||
Extract Constant Z.abs => "abs_float".
|
||||
Extract Constant Z.min => "min".
|
||||
Extract Constant Z.max => "max".
|
||||
Extract Constant Z.compare =>
|
||||
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
|
||||
|
||||
Extract Constant Pos.add => "(+.)".
|
||||
Extract Constant Pos.succ => "(+.) 1.".
|
||||
Extract Constant Pos.pred => "(fun x -> x -. 1.)".
|
||||
Extract Constant Pos.sub => "(-.)".
|
||||
Extract Constant Pos.mul => "( *. )".
|
||||
Extract Constant Pos.min => "min".
|
||||
Extract Constant Pos.max => "max".
|
||||
Extract Constant Pos.compare =>
|
||||
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
|
||||
Extract Constant Pos.compare_cont =>
|
||||
"fun x y c -> if x=y then c else if x<y then Lt else Gt".
|
||||
|
||||
Extract Constant N.add => "(+.)".
|
||||
Extract Constant N.succ => "(+.) 1.".
|
||||
Extract Constant N.pred => "(fun x -> x -. 1.)".
|
||||
Extract Constant N.sub => "(-.)".
|
||||
Extract Constant N.mul => "( *. )".
|
||||
Extract Constant N.min => "min".
|
||||
Extract Constant N.max => "max".
|
||||
Extract Constant N.div => "(fun x y -> if x = 0. then 0. else floor (x /. y))".
|
||||
Extract Constant N.modulo => "mod_float".
|
||||
Extract Constant N.compare =>
|
||||
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
|
||||
|
||||
Extract Inductive Fappli_IEEE.binary_float => float [
|
||||
"(fun s -> if s then (0.) else (-0.))"
|
||||
"(fun s -> if s then infinity else neg_infinity)"
|
||||
"nan"
|
||||
"(fun (s, m, e) -> failwith ""FIXME: No extraction from binary float allowed yet."")"
|
||||
].
|
||||
|
||||
Extract Constant JsNumber.of_int => "fun x -> x".
|
||||
|
||||
Extract Constant JsNumber.nan => "nan".
|
||||
Extract Constant JsNumber.zero => "0.".
|
||||
Extract Constant JsNumber.neg_zero => "(-0.)".
|
||||
Extract Constant JsNumber.one => "1.".
|
||||
Extract Constant JsNumber.infinity => "infinity".
|
||||
Extract Constant JsNumber.neg_infinity => "neg_infinity".
|
||||
Extract Constant JsNumber.max_value => "max_float".
|
||||
Extract Constant JsNumber.min_value => "(Int64.float_of_bits Int64.one)".
|
||||
Extract Constant JsNumber.pi => "(4. *. atan 1.)".
|
||||
Extract Constant JsNumber.e => "(exp 1.)".
|
||||
Extract Constant JsNumber.ln2 => "(log 2.)".
|
||||
Extract Constant JsNumber.floor => "floor".
|
||||
Extract Constant JsNumber.absolute => "abs_float".
|
||||
|
||||
Extract Constant JsNumber.from_string =>
|
||||
"(fun s ->
|
||||
try
|
||||
let s = (String.concat """" (List.map (String.make 1) s)) in
|
||||
if s = """" then 0. else float_of_string s
|
||||
with Failure ""float_of_string"" -> nan)
|
||||
(* Note that we're using `float_of_string' there, which does not have the same
|
||||
behavior than JavaScript. For instance it will read ""022"" as 22 instead of
|
||||
18, which should be the JavaScript result for it. *)".
|
||||
|
||||
Extract Constant JsNumber.to_string =>
|
||||
"(fun f ->
|
||||
prerr_string (""Warning: JsNumber.to_string called. This might be responsible for errors. Argument value: "" ^ string_of_float f ^ ""."");
|
||||
prerr_newline();
|
||||
let string_of_number n =
|
||||
let sfn = string_of_float n in
|
||||
(if (sfn = ""inf"") then ""Infinity"" else
|
||||
if (sfn = ""-inf"") then ""-Infinity"" else
|
||||
if (sfn = ""nan"") then ""NaN"" else
|
||||
let inum = int_of_float n in
|
||||
if (float_of_int inum = n) then (string_of_int inum) else (string_of_float n)) in
|
||||
let ret = ref [] in (* Ugly, but the API for OCaml string is not very functional... *)
|
||||
String.iter (fun c -> ret := c :: !ret) (string_of_number f);
|
||||
List.rev !ret)
|
||||
(* Note that this is ugly, we should use the spec of JsNumber.to_string here (9.8.1). *)".
|
||||
|
||||
Extract Constant JsNumber.add => "(+.)".
|
||||
Extract Constant JsNumber.sub => "(-.)".
|
||||
Extract Constant JsNumber.mult => "( *. )".
|
||||
Extract Constant JsNumber.div => "(/.)".
|
||||
Extract Constant JsNumber.fmod => "mod_float".
|
||||
Extract Constant JsNumber.neg => "(~-.)".
|
||||
Extract Constant JsNumber.sign => "(fun f -> float_of_int (compare f 0.))".
|
||||
Extract Constant JsNumber.number_comparable => "(fun n1 n2 -> 0 = compare n1 n2)".
|
||||
Extract Constant JsNumber.lt_bool => "(<)".
|
||||
|
||||
Extract Constant JsNumber.to_int32 =>
|
||||
"fun n ->
|
||||
match classify_float n with
|
||||
| FP_normal | FP_subnormal ->
|
||||
let i32 = 2. ** 32. in
|
||||
let i31 = 2. ** 31. in
|
||||
let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
|
||||
let int32bit =
|
||||
let smod = mod_float posint i32 in
|
||||
if smod < 0. then smod +. i32 else smod
|
||||
in
|
||||
(if int32bit >= i31 then int32bit -. i32 else int32bit)
|
||||
| _ -> 0.". (* LATER: do in Coq. Spec is 9.5, p. 47.*)
|
||||
|
||||
Extract Constant JsNumber.to_uint32 =>
|
||||
"fun n ->
|
||||
match classify_float n with
|
||||
| FP_normal | FP_subnormal ->
|
||||
let i32 = 2. ** 32. in
|
||||
let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
|
||||
let int32bit =
|
||||
let smod = mod_float posint i32 in
|
||||
if smod < 0. then smod +. i32 else smod
|
||||
in
|
||||
int32bit
|
||||
| _ -> 0.". (* LAER: do in Coq. Spec is 9.6, p47.*)
|
||||
|
||||
Extract Constant JsNumber.modulo_32 => "(fun x -> let r = mod_float x 32. in if x < 0. then r +. 32. else r)".
|
||||
Extract Constant JsNumber.int32_bitwise_not => "fun x -> Int32.to_float (Int32.lognot (Int32.of_float x))".
|
||||
Extract Constant JsNumber.int32_bitwise_and => "fun x y -> Int32.to_float (Int32.logand (Int32.of_float x) (Int32.of_float y))".
|
||||
Extract Constant JsNumber.int32_bitwise_or => "fun x y -> Int32.to_float (Int32.logor (Int32.of_float x) (Int32.of_float y))".
|
||||
Extract Constant JsNumber.int32_bitwise_xor => "fun x y -> Int32.to_float (Int32.logxor (Int32.of_float x) (Int32.of_float y))".
|
||||
Extract Constant JsNumber.int32_left_shift => "(fun x y -> Int32.to_float (Int32.shift_left (Int32.of_float x) (int_of_float y)))".
|
||||
Extract Constant JsNumber.int32_right_shift => "(fun x y -> Int32.to_float (Int32.shift_right (Int32.of_float x) (int_of_float y)))".
|
||||
Extract Constant JsNumber.uint32_right_shift =>
|
||||
"(fun x y ->
|
||||
let i31 = 2. ** 31. in
|
||||
let i32 = 2. ** 32. in
|
||||
let newx = if x >= i31 then x -. i32 else x in
|
||||
let r = Int32.to_float (Int32.shift_right_logical (Int32.of_float newx) (int_of_float y)) in
|
||||
if r < 0. then r +. i32 else r)".
|
||||
|
||||
Extract Constant int_of_char => "(fun c -> float_of_int (int_of_char c))".
|
||||
|
||||
Extract Constant ascii_comparable => "(=)".
|
||||
Extract Constant lt_int_decidable => "(<)".
|
||||
Extract Constant le_int_decidable => "(<=)".
|
||||
Extract Constant ge_nat_decidable => "(>=)".
|
||||
|
||||
(* TODO ARTHUR: This TLC lemma does not extract to something computable... whereas it should! *)
|
||||
Extract Constant prop_eq_decidable => "(=)".
|
||||
|
||||
Extract Constant env_loc_global_env_record => "0".
|
||||
|
||||
(* The following functions make pattern matches with floats and shall thus be removed. *)
|
||||
Extraction Inline Fappli_IEEE.Bplus Fappli_IEEE.binary_normalize Fappli_IEEE_bits.b64_plus.
|
||||
Extraction Inline Fappli_IEEE.Bmult Fappli_IEEE.Bmult_FF Fappli_IEEE_bits.b64_mult.
|
||||
Extraction Inline Fappli_IEEE.Bdiv Fappli_IEEE_bits.b64_div.
|
||||
|
||||
(* New options for the interpreter to work in Coq 8.4 *)
|
||||
Set Extraction AccessOpaque.
|
||||
|
||||
(* These parameters are implementation-dependant according to the spec.
|
||||
I've chosed some very simple values, but we could choose another thing for them. *)
|
||||
Extract Constant object_prealloc_global_proto => "(Coq_value_prim Coq_prim_null)".
|
||||
Extract Constant object_prealloc_global_class => "(
|
||||
let rec aux s = function
|
||||
| 0 -> []
|
||||
| n -> let n' = n - 1 in
|
||||
s.[n'] :: aux s n'
|
||||
in let aux2 s =
|
||||
List.rev (aux s (String.length s))
|
||||
in aux2 ""GlobalClass"")".
|
||||
|
||||
|
||||
(* Parsing *)
|
||||
Extract Constant parse_pickable => "(fun s strict ->
|
||||
let str = String.concat """" (List.map (String.make 1) s) in
|
||||
try
|
||||
let parserExp = Parser_main.exp_from_string ~force_strict:strict str in
|
||||
Some (JsSyntaxInfos.add_infos_prog strict
|
||||
(Translate_syntax.exp_to_prog parserExp))
|
||||
with
|
||||
(* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
|
||||
| Parser.ParserFailure _
|
||||
| Parser.InvalidArgument ->
|
||||
prerr_string (""Warning: Parser error on eval. Input string: \"""" ^ str ^ ""\""\n"");
|
||||
None
|
||||
)".
|
||||
|
||||
|
||||
(* Debugging *)
|
||||
Extract Inlined Constant not_yet_implemented_because => "(fun s ->
|
||||
print_endline (__LOC__ ^ "": Not implemented because: "" ^ Prheap.string_of_char_list s) ;
|
||||
Coq_result_not_yet_implemented)".
|
||||
Extract Inlined Constant impossible_because => "(fun s ->
|
||||
print_endline (__LOC__ ^ "": Stuck because: "" ^ Prheap.string_of_char_list s) ;
|
||||
Coq_result_impossible)".
|
||||
Extract Inlined Constant impossible_with_heap_because => "(fun s message ->
|
||||
print_endline (__LOC__ ^ "": Stuck!\nState: "" ^ Prheap.prstate true s
|
||||
^ ""\nMessage:\t"" ^ Prheap.string_of_char_list message) ;
|
||||
Coq_result_impossible)".
|
||||
|
||||
|
||||
(* Final Extraction *)
|
||||
Extraction Blacklist string list bool.
|
||||
Separate Extraction runs run_javascript.
|
||||
|
||||
|
||||
|
||||
(* -- LATER: extract inequality_test_string in more efficient way*)
|
||||
|
||||
1051
samples/Coq/JsNumber.v
Normal file
1051
samples/Coq/JsNumber.v
Normal file
File diff suppressed because it is too large
Load Diff
1766
samples/Coq/JsPrettyInterm.v
Normal file
1766
samples/Coq/JsPrettyInterm.v
Normal file
File diff suppressed because it is too large
Load Diff
42
samples/Coq/Main.v
Normal file
42
samples/Coq/Main.v
Normal file
@@ -0,0 +1,42 @@
|
||||
Require Import FunctionNinjas.All.
|
||||
Require Import ListString.All.
|
||||
Require Import Computation.
|
||||
|
||||
Import C.Notations.
|
||||
|
||||
Definition error (message : LString.t) : C.t :=
|
||||
do_call! Command.ShowError message in
|
||||
ret.
|
||||
|
||||
Definition main : C.t :=
|
||||
call! card_is_valid := Command.AskCard in
|
||||
if card_is_valid then
|
||||
call! pin := Command.AskPIN in
|
||||
match pin with
|
||||
| None => error @@ LString.s "No PIN given."
|
||||
| Some pin =>
|
||||
call! pin_is_valid := Command.CheckPIN pin in
|
||||
if pin_is_valid then
|
||||
call! ask_amount := Command.AskAmount in
|
||||
match ask_amount with
|
||||
| None => error @@ LString.s "No amount given."
|
||||
| Some amount =>
|
||||
call! amount_is_valid := Command.CheckAmount amount in
|
||||
if amount_is_valid then
|
||||
call! card_is_given := Command.GiveCard in
|
||||
if card_is_given then
|
||||
call! amount_is_given := Command.GiveAmount amount in
|
||||
if amount_is_given then
|
||||
ret
|
||||
else
|
||||
error @@ LString.s "Cannot give you the amount. Please contact your bank."
|
||||
else
|
||||
error @@ LString.s "Cannot give you back the card. Please contact your bank."
|
||||
else
|
||||
error @@ LString.s "Invalid amount."
|
||||
end
|
||||
else
|
||||
error @@ LString.s "Invalid PIN."
|
||||
end
|
||||
else
|
||||
error @@ LString.s "Invalid card.".
|
||||
@@ -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 *)
|
||||
@@ -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 *)
|
||||
@@ -1,2 +0,0 @@
|
||||
Require Export Sorted.
|
||||
Require Export Mergesort.
|
||||
62
samples/Coq/Spec.v
Normal file
62
samples/Coq/Spec.v
Normal file
@@ -0,0 +1,62 @@
|
||||
(** Specifications. *)
|
||||
Require Import Coq.Lists.List.
|
||||
Require Import Coq.Strings.Ascii.
|
||||
Require Import FunctionNinjas.All.
|
||||
Require Import ListString.All.
|
||||
Require Import Computation.
|
||||
|
||||
Import ListNotations.
|
||||
Local Open Scope char.
|
||||
|
||||
(** A run is an execution of the program with explicit answers for the
|
||||
system calls. *)
|
||||
Module Run.
|
||||
(** We define a run by induction on the structure of a computation. *)
|
||||
Inductive t : C.t -> Type :=
|
||||
| Ret : t C.Ret
|
||||
| Call : forall (command : Command.t) (answer : Command.answer command)
|
||||
{handler : Command.answer command -> C.t}, t (handler answer) ->
|
||||
t (C.Call command handler).
|
||||
|
||||
(** The trace of a run. *)
|
||||
Fixpoint trace {x : C.t} (run : t x)
|
||||
: list {command : Command.t & Command.answer command} :=
|
||||
match run with
|
||||
| Ret => []
|
||||
| Call command answer _ run => existT _ command answer :: trace run
|
||||
end.
|
||||
End Run.
|
||||
|
||||
Module Temporal.
|
||||
Module All.
|
||||
Inductive t (P : Command.t -> Prop) : C.t -> Prop :=
|
||||
| Ret : t P C.Ret
|
||||
| Call : forall (c : Command.t) (h : Command.answer c -> C.t),
|
||||
P c -> (forall a, t P (h a)) ->
|
||||
t P (C.Call c h).
|
||||
End All.
|
||||
|
||||
Module One.
|
||||
Inductive t (P : Command.t -> Prop) : C.t -> Prop :=
|
||||
| CallThis : forall (c : Command.t) (h : Command.answer c -> C.t),
|
||||
P c ->
|
||||
t P (C.Call c h)
|
||||
| CallOther : forall (c : Command.t) (h : Command.answer c -> C.t),
|
||||
(forall a, t P (h a)) ->
|
||||
t P (C.Call c h).
|
||||
End One.
|
||||
|
||||
Module Then.
|
||||
Inductive t (P1 P2 : Command.t -> Prop) : C.t -> Prop :=
|
||||
| Ret : t P1 P2 C.Ret
|
||||
| Call : forall (c : Command.t) (h : Command.answer c -> C.t),
|
||||
(forall a, t P1 P2 (h a)) ->
|
||||
t P1 P2 (C.Call c h)
|
||||
| CallThen : forall (c : Command.t) (h : Command.answer c -> C.t),
|
||||
P1 c -> (forall a, One.t P2 (h a)) ->
|
||||
t P1 P2 (C.Call c h).
|
||||
End Then.
|
||||
End Temporal.
|
||||
|
||||
Module CardBeforeMoney.
|
||||
End CardBeforeMoney.
|
||||
@@ -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.
|
||||
Reference in New Issue
Block a user