(*

Midland Graduate School 2008: COQ

*)

Section le.

Fixpoint le (m n:nat) {struct m} : bool :=
  match m with
    | 0 => true
    | S m' => match n with
               | 0 => false
               | S n' => le m' n'
              end
    end.

Eval compute in (le 3 4).

Inductive Le : nat -> nat -> Prop :=
  | le0 : forall n:nat, Le 0 n
  | leS : forall m n:nat, Le m n -> Le (S m) (S n).

Goal Le 3 4.
apply leS.
apply leS.
apply leS.
apply le0.
Save le34.

Print le34.

Goal ~(Le 1 0).
intro.
inversion H.
Qed.

Hint Resolve le0.
Hint Resolve leS.

Goal Le 3 4.
auto.
Save le34'.

Print le34'.

Lemma le_refl : forall n:nat,Le n n.
induction n.
auto.
auto.
Qed.

Lemma le_compl : forall i j:nat,Le i j -> le i j = true.
intros.
induction H.
auto.
auto.
Qed.

Lemma le_sound : forall i j:nat,le i j = true -> Le i j.
induction i.
auto.
intro j.
case_eq j.
intros.
simpl in H0.
discriminate H0.
intros.
auto.
Qed.

Lemma le_ok : forall i j:nat,Le i j <-> le i j = true.
split.
apply le_compl.
apply le_sound.
Qed.

Program Fixpoint le' (m n:nat) {struct m} : {Le m n} + {~ Le m n} :=
   match m with
     | 0 => left _ _
     | S m' => match n with
                 | 0 => right _ _
                 | S n' => match le' m' n' with
                             | left _ => left _ _
                             | right _ => right _ _
                           end
               end
   end.

Next Obligation.
intro.
inversion H.
Defined.

Next Obligation.
intro.
apply wildcard'.
inversion H.
auto.
Defined.

Eval compute in (le' 3 4).

End le.

Section subsets.

Require Import Arith.
Require Import Coq.subtac.Utils.

Program Fixpoint div2 (n : nat) : 
  { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
  match n with
    | S (S p) => S (div2 p)
    | _ => O
  end.

Next Obligation.
destruct_call div2.
simpl.
case o.
intros.
left.
rewrite H.
ring.
intros.
right.
rewrite H.
ring.
Defined.

Next Obligation.
case_eq n.
left.
auto.
intros.
rewrite H0 in H.
case_eq n0.
intros.
right.
reflexivity.
intros.
rewrite H1 in H.
absurd (S (S n1) = S( S n1)).
apply H.
reflexivity.
Defined.

Section vec.

Set Implicit Arguments.

Require Import List.

Variable A:Set.

(*
Fixpoint nth (n:nat) (l:list A) {struct l}: A :=
  match l with
  | nil => error
  | a::l' => match n with
             | 0 => a
             | S n' => nth n' l'
             end
  end.
*)

Inductive Vec : nat -> Set :=
  | vnil : Vec 0
  | vcons : forall n:nat,A -> Vec n -> Vec (S n).

Program Fixpoint vappend (m n:nat)(xs : Vec m)(bs:Vec n) {struct xs}
  : Vec (m + n) :=
   match xs with
     | vnil => bs
     | vcons _ a ys => vcons a (vappend ys bs)
   end.

Inductive Fin : nat -> Set :=
  | fz : forall n:nat,Fin (1 + n)
  | fs : forall n:nat,Fin n -> Fin (1 + n).

Program Fixpoint vnth (m:nat)(xs : Vec m)(i : Fin m) {struct xs} : A :=
  match xs with
    | vnil => _
    | vcons _ a ys => 
         match i with 
           | fz _ => a
           | fs _ i => vnth ys i
         end
  end.

Next Obligation.
inversion i.
Qed.