(* 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.