443 lines
9.6 KiB
Coq
443 lines
9.6 KiB
Coq
From LF Require Export Induction.
|
|
Module NatList.
|
|
|
|
Inductive natprod : Type :=
|
|
| pair (n1 n2 : nat).
|
|
|
|
Definition fst (p : natprod) : nat :=
|
|
match p with
|
|
| pair x y => x
|
|
end.
|
|
|
|
Definition snd (p : natprod) : nat :=
|
|
match p with
|
|
| pair x y => y
|
|
end.
|
|
|
|
Notation "( x , y )" := (pair x y).
|
|
|
|
Definition swap_pair (p : natprod) : natprod :=
|
|
match p with
|
|
| (x, y) => (y, x)
|
|
end.
|
|
|
|
Theorem surjective_pairing : forall (n m : nat),
|
|
(n, m) = (fst (n, m), snd (n, m)).
|
|
Proof.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem snd_fst_is_swap : forall (p : natprod),
|
|
(snd p, fst p) = swap_pair p.
|
|
Proof.
|
|
intros [n m].
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem fst_swap_is_snd : forall (p : natprod),
|
|
fst (swap_pair p) = snd p.
|
|
Proof.
|
|
intros [n m].
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Inductive natlist : Type :=
|
|
| nil
|
|
| cons (n : nat) (l : natlist).
|
|
|
|
Notation "x :: l" := (cons x l)
|
|
(at level 60, right associativity).
|
|
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
|
|
|
|
Fixpoint repeat (n count : nat) : natlist :=
|
|
match count with
|
|
| 0 => nil
|
|
| S count' => n :: (repeat n count')
|
|
end.
|
|
|
|
Fixpoint length (l : natlist) : nat :=
|
|
match l with
|
|
| nil => 0
|
|
| _ :: t => S (length t)
|
|
end.
|
|
|
|
Fixpoint app (l1 l2 : natlist) : natlist :=
|
|
match l1 with
|
|
| nil => l2
|
|
| h :: t => h :: (app t l2)
|
|
end.
|
|
|
|
Notation "x ++ y" := (app x y)
|
|
(right associativity, at level 60).
|
|
|
|
Definition hd (default : nat) (l : natlist) : nat :=
|
|
match l with
|
|
| nil => default
|
|
| h :: t => h
|
|
end.
|
|
|
|
Definition tl (l: natlist) : natlist :=
|
|
match l with
|
|
| nil => nil
|
|
| h :: t => t
|
|
end.
|
|
|
|
Fixpoint nonzeros (l : natlist) : natlist :=
|
|
match l with
|
|
| nil => nil
|
|
| 0 :: t => nonzeros t
|
|
| h :: t => h :: nonzeros t
|
|
end.
|
|
|
|
Fixpoint odd (n : nat): bool :=
|
|
match n with
|
|
| O => false
|
|
| S n' => negb (odd n')
|
|
end.
|
|
|
|
Fixpoint oddmembers (l : natlist) : natlist :=
|
|
match l with
|
|
| nil => nil
|
|
| h :: t => if odd (h)
|
|
then h :: oddmembers t
|
|
else oddmembers t
|
|
end.
|
|
|
|
Definition countoddmembers (l: natlist) : nat :=
|
|
length (oddmembers l).
|
|
|
|
Fixpoint alternate (l1 l2 : natlist) : natlist :=
|
|
match l1, l2 with
|
|
| nil, nil => nil
|
|
| nil, l2' => l2'
|
|
| l1', nil => l1'
|
|
| h1 :: t1, h2 :: t2 => h1 :: h2 :: alternate t1 t2
|
|
end.
|
|
|
|
Definition bag := natlist.
|
|
|
|
Fixpoint count (v : nat) (s : bag) : nat :=
|
|
match s with
|
|
| nil => 0
|
|
| h :: t => if eqb v h
|
|
then S (count v t)
|
|
else count v t
|
|
end.
|
|
|
|
Definition sum : bag -> bag -> bag := app.
|
|
|
|
Definition add : nat -> bag -> bag := cons.
|
|
|
|
Fixpoint member (v : nat) (s : bag) : bool :=
|
|
match s with
|
|
| nil => false
|
|
| h :: t => if eqb v h
|
|
then true
|
|
else member v t
|
|
end.
|
|
|
|
Fixpoint remove_one (v : nat) (s : bag) : bag :=
|
|
match s with
|
|
| nil => nil
|
|
| h :: t => if eqb v h
|
|
then t
|
|
else h :: remove_one v t
|
|
end.
|
|
|
|
Fixpoint remove_all (v : nat) (s : bag) : bag :=
|
|
match s with
|
|
| nil => nil
|
|
| h :: t => if eqb v h
|
|
then remove_all v t
|
|
else h :: remove_all v t
|
|
end.
|
|
|
|
Fixpoint included (s1 : bag) (s2 : bag) : bool :=
|
|
match s1 with
|
|
| nil => true
|
|
| h :: t => if member h s2
|
|
then included t s2
|
|
else false
|
|
end.
|
|
|
|
Theorem add_inc_count : forall (n : nat) (b : bag),
|
|
count n (add n b) = S (count n b).
|
|
Proof.
|
|
intros n [ |[]] ; simpl ; rewrite eqb_refl ; reflexivity.
|
|
Qed.
|
|
|
|
Theorem nil_app : forall l : natlist,
|
|
nil ++ l = l.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Definition pred n : nat :=
|
|
match n with
|
|
| 0 => 0
|
|
| S n' => n'
|
|
end.
|
|
|
|
Theorem tl_length_pred : forall l : natlist,
|
|
pred (length l) = length (tl l).
|
|
Proof.
|
|
intros [|] ; reflexivity.
|
|
Qed.
|
|
|
|
Theorem app_assoc : forall l1 l2 l3 : natlist,
|
|
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
|
|
Proof.
|
|
intros l1 l2 l3.
|
|
induction l1 as [ | n l1' IHl1'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHl1'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Fixpoint rev (l: natlist) : natlist :=
|
|
match l with
|
|
| nil => nil
|
|
| h :: t => rev t ++ [h]
|
|
end.
|
|
|
|
Theorem app_length : forall l1 l2 : natlist,
|
|
length (l1 ++ l2) = (length l1) + (length l2).
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1 as [ | n l1' IHl1'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHl1'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem rev_length : forall l : natlist,
|
|
length (rev l) = length l.
|
|
Proof.
|
|
induction l as [ | n l' IHl'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite app_length.
|
|
simpl.
|
|
rewrite IHl'.
|
|
rewrite <- plus_n_Sm.
|
|
rewrite add_0_r.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem app_nil_r : forall l : natlist,
|
|
l ++ nil = l.
|
|
Proof.
|
|
induction l as [ | n l' IHl'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHl'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem rev_app_distr: forall l1 l2 : natlist,
|
|
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1 as [ | n l1' IHl1'].
|
|
- simpl.
|
|
rewrite app_nil_r.
|
|
reflexivity.
|
|
- simpl.
|
|
rewrite IHl1'.
|
|
rewrite app_assoc.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem rev_involutive : forall l : natlist,
|
|
rev (rev l) = l.
|
|
Proof.
|
|
induction l as [ | n l' IHl'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite rev_app_distr.
|
|
simpl.
|
|
rewrite IHl'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
|
|
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
|
|
Proof.
|
|
intros.
|
|
repeat rewrite app_assoc.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem nonzeros_app : forall l1 l2 : natlist,
|
|
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1 as [ | h t IHl1'].
|
|
- reflexivity.
|
|
- destruct h as [ | ] ; simpl; rewrite IHl1'; reflexivity.
|
|
Qed.
|
|
|
|
Fixpoint eqblist (l1 l2 : natlist) : bool :=
|
|
match l1, l2 with
|
|
| nil, nil => true
|
|
| nil, _ => false
|
|
| _, nil => false
|
|
| h1 :: t1, h2 :: t2 => if eqb h1 h2
|
|
then eqblist t1 t2
|
|
else false
|
|
end.
|
|
|
|
Theorem eqblist_refl : forall l : natlist,
|
|
eqblist l l = true.
|
|
Proof.
|
|
induction l as [ | h t IHt].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite eqb_refl.
|
|
rewrite IHt.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem count_member_nonzero : forall (s : bag),
|
|
1 <=? (count 1 (1 :: s)) = true.
|
|
|
|
Proof.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem leb_n_Sn : forall n,
|
|
n <=? (S n) = true.
|
|
Proof.
|
|
induction n as [ | n' IHn'].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHn'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem remove_does_not_increase_count : forall (s : bag),
|
|
(count 0 (remove_one 0 s)) <=? (count 0 s) = true.
|
|
Proof.
|
|
induction s as [ | [ |h] t IHt].
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite leb_n_Sn.
|
|
reflexivity.
|
|
- simpl.
|
|
rewrite IHt.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem bag_count_sum : forall (b1 b2 : bag),
|
|
count 0 (sum b1 b2) = count 0 b1 + count 0 b2.
|
|
Proof.
|
|
intros b1 b2.
|
|
induction b1 as [ | h t IHt].
|
|
- reflexivity.
|
|
- destruct h as [ |n] ; simpl ; rewrite IHt ; reflexivity.
|
|
Qed.
|
|
|
|
Theorem involution_injective : forall (f : nat -> nat),
|
|
(forall n : nat, n = f (f n)) ->
|
|
(forall n1 n2 : nat, f n1 = f n2 -> n1 = n2).
|
|
Proof.
|
|
intros f H n1 n2 H1.
|
|
rewrite H.
|
|
rewrite <- H1.
|
|
rewrite <- H.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem rev_injective : forall (l1 l2 : natlist),
|
|
rev l1 = rev l2 -> l1 = l2.
|
|
Proof.
|
|
intros l1 l2 H.
|
|
rewrite <- rev_involutive.
|
|
rewrite <- H.
|
|
rewrite rev_involutive.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Inductive natoption : Type :=
|
|
| Some (n : nat)
|
|
| None.
|
|
|
|
Fixpoint nth_error (l : natlist) (n : nat) : natoption :=
|
|
match l with
|
|
| nil => None
|
|
| a :: l' => match n with
|
|
| 0 => Some a
|
|
| S n' => nth_error l' n'
|
|
end
|
|
end.
|
|
|
|
Definition option_elim (d : nat) (o : natoption) : nat :=
|
|
match o with
|
|
| Some n' => n'
|
|
| None => d
|
|
end.
|
|
|
|
Definition hd_error (l : natlist) : natoption :=
|
|
match l with
|
|
| nil => None
|
|
| h :: _ => Some h
|
|
end.
|
|
|
|
Theorem option_elim_hd : forall (l : natlist) (default: nat),
|
|
hd default l = option_elim default (hd_error l).
|
|
Proof.
|
|
intros [ | h tl] d ; reflexivity.
|
|
Qed.
|
|
End NatList.
|
|
|
|
Module PartialMap.
|
|
Export NatList.
|
|
|
|
Inductive id : Type :=
|
|
| Id (n : nat).
|
|
|
|
Definition eqb_id (x1 x2 : id) :=
|
|
match x1, x2 with
|
|
| Id n1, Id n2 => n1 =? n2
|
|
end.
|
|
|
|
Theorem eqb_id_refl : forall x, eqb_id x x = true.
|
|
Proof.
|
|
intros [x].
|
|
simpl.
|
|
rewrite eqb_refl.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Inductive partial_map : Type :=
|
|
| empty
|
|
| record (i : id) (v : nat) (m : partial_map).
|
|
|
|
Definition update (d : partial_map)
|
|
(x : id) (value : nat)
|
|
: partial_map :=
|
|
record x value d.
|
|
|
|
Fixpoint find (x : id) (d : partial_map) : natoption :=
|
|
match d with
|
|
| empty => None
|
|
| record y v d' => if eqb_id x y
|
|
then Some v
|
|
else find x d'
|
|
end.
|
|
|
|
Theorem update_eq :
|
|
forall (d : partial_map) (x : id) (v : nat),
|
|
find x (update d x v) = Some v.
|
|
Proof.
|
|
intros [ | [] ] [] ; simpl ; rewrite eqb_refl ; reflexivity.
|
|
Qed.
|
|
|
|
Theorem update_neq :
|
|
forall (d : partial_map) (x y : id) (o : nat),
|
|
eqb_id x y = false -> find x (update d y o) = find x d.
|
|
Proof.
|
|
intros [ | [] ] [] [] o H ; simpl ; simpl in H ; rewrite H ; reflexivity.
|
|
Qed.
|
|
|
|
End PartialMap.
|