Parameter A : Type. Definition head (d:A) (l:list A) : A := match l with | nil => d (* dummy value *) | cons x l' => x end. Definition tail (l:list A) : list A := match l with | nil => nil (* dummy value *) | cons x l' => l' end. Lemma inj_list (x1 x2:A) l1 l2 : cons x1 l1 = cons x2 l2 -> x1=x2 /\ l1=l2. split. apply f_equal with (f:=head x1) in H. simpl in H. assumption. apply f_equal with (f:=tail) in H. simpl in H. assumption. Qed. Definition is_nil (l:list A) := match l with | nil => True | cons _ _ => False end. Lemma discr_list (x:A) l : nil <> cons x l. intro e. change (is_nil (cons x l)). (* is_nil (cons x l) is convertible to False *) rewrite <- e. simpl. trivial. Qed. Parameter lambda : Type. Parameter Lam : (lambda->lambda) -> lambda. Parameter match_lambda : forall P:lambda -> Type, (forall f:lambda->lambda, P (Lam f)) -> forall l, P l. Parameter lambda_eq : forall P H f, match_lambda P H (Lam f) = H f. Definition app (t1 t2:lambda) : lambda := match_lambda (fun _ => lambda) (fun f => f t2) t1. Lemma beta_eq f x : app (Lam f) x = f x. unfold app. rewrite lambda_eq. reflexivity. Qed. Lemma has_fix (f:lambda->lambda) : exists t, f t = t. (* In the pure lambda-calculus Y f is a fixpoint of f *) exists (app (Lam (fun x => f (app x x))) (Lam (fun x => f (app x x)))). symmetry. apply beta_eq with (f:=(fun x=>f(app x x))). Qed. (* Lam and app (and the equation beta_eq) suggest that lambda and (lambda->lambda) are isomorphic. By Cantor's paradox (A and A->Prop cannot be isomorphic), there is no solution if the cardinality of lambda is at least 2. In contrast, unit and unit->unit are isomorphic (but we need functional extensionality, which is not provable in Coq). *) Definition L : Type := unit. Definition Li (f:L->L) : L := tt. Definition Lm (P:L->Type) (H:forall f:L->L, P(Li f)) (l:L) : P l := match l return P l with | tt => H (fun _ => tt) end. Parameter fun_ext : forall (A B:Type) (f g:A->B), (forall x, f x = g x) -> f=g. Lemma L_eq P H f : Lm P H (Li f) = H f. unfold Li, Lm. f_equal. apply fun_ext; intros x. destruct (f x). reflexivity. Qed. Parameter rec_lambda : forall P:lambda->Type, (forall f, (forall x, P (f x)) -> P (Lam f)) -> forall l, P l. Lemma paradox : False. apply rec_lambda with (P:=fun _ => False) (l:=Lam(fun x=>x)). intros f Hrecf. apply Hrecf. exact (Lam f). Qed. Inductive id := Id (_:forall A:Prop,A->A). (* The elimination rulw for id allows to get an expression of type forall A:Prop,A->A which, instantiating A with id (id has type Prop), yields an expression of type lambda->lambda. So, without special care, the above paradox applies. Fortunately, it is ruled out because Coq the argument of Id has a type not ending with id, and so is not considered as a possible subterm of i *) Fail Fixpoint F (i:id) : False:= match i with | Id f => F (f id i) end. (* leq is accepted, by structural induction on n (or p) exp is not accepted: (S n) is not a subterm of n (although the definition exp makes sense since p increases from 0 and will eventually become larger than n) ackermann1 is not accepted: recursive call (f n' _) requires that the fixpoint is by induction on n, but then the recursive call (f n m') is not valid (n doesn't decrease) ackermann2 is accepted f takes care of recursive calls where n decreases. The inner fixpoint g takes care of calls where m decreases and n remains the same. *) Inductive W (A:Type) (B:A -> Type) : Type := node : forall (a:A), (B a -> W A B) -> W A B. Check W_rect : forall A B (P:W A B->Type), (forall a f, (forall i:B a,P(f i)) -> P (node A B a f)) -> forall w:W A B, P w. Definition Anat := bool. Definition Bnat (a:Anat) : Type := if a then unit else False. Definition Wnat := W Anat Bnat. Definition W0 : Wnat := node _ _ false (fun i:False => False_rect _ i). Definition WS (n:Wnat) : Wnat := node _ _ true (fun _ => n). (* The "A" part contains both the constructor selector and the constructor arguments that are not recursive *) Inductive Atree := bleaf | bnode (_:A). Definition Btree a : Type := match a with | bleaf => False (* leafs have no subtree *) | bnode l => bool (* nodes have two subtrees *) end. Definition bintree := W Atree Btree. Definition binleaf : bintree := node _ _ bleaf (fun i:False => False_rect _ i). Definition binnode (lft : bintree) (lab:A) (rght:bintree) : bintree := node _ _ (bnode lab) (fun b:bool => if b then lft else rght). Definition f1 : unit -> Wnat := fun _ => W0. Definition f2 : unit -> Wnat := fun x:unit => match x with tt => W0 end. Lemma f1_f2_ext_eq : forall x, f1 x = f2 x. destruct x; reflexivity. Qed. Lemma f1_f2_not_conv : f1=f2. Fail reflexivity. (* reflexivity would succeed if f1 and f2 were convertible *) Abort. (* Regarding Wnat, there are inhabitants of that type that are neither W0 nor WS n for some n:Wnat *) Definition Wone := node _ _ true f1. (* is the normal form of WS W0 *) Definition Wone' := node _ _ true f2. (* Wone' has the same structure as Wone (same "nat"-constructor, and same children), but they are not provably equal (unless we assume functional extensionality). A consequence of this is that the dependent recursor for Wnat: forall P:Wnat->Prop, P W0 -> (forall n, P n -> P (WS n)) -> forall n, P n is not provable. However, using fun_ext, it is provable... *) Definition Wnat_rect (P:Wnat->Type) (H0 : P W0) (HS : forall n, P n -> P (WS n)) (n:Wnat) : P n. induction n. destruct a. (* The conclusion is not of the form WS n, because w may not be of the form (fun _ => ..) *) replace w with (fun _:unit => w tt). (* ...but is provably equal to a term of that form *) apply HS. apply (X tt). apply fun_ext; intros x. destruct x; reflexivity. replace w with (fun i:False => False_rect Wnat i). apply H0. apply fun_ext; intros x. contradiction. Defined. (* However, proving the computational rule for Wnat_rect, requires to show some specific property about fun_ext... *) Lemma Wnat_rect_eq0 P H0 HS : Wnat_rect P H0 HS W0 = H0. unfold Wnat_rect; simpl. replace (fun_ext False Wnat (fun i => False_rect Wnat i) (fun i => False_rect (W bool Bnat) i) (fun x => False_ind (False_rect Wnat x = False_rect (W bool Bnat) x) x)) with (eq_refl (fun i => False_rect Wnat i)). reflexivity. admit. Abort. Lemma Wnat_rect_eqS P H0 HS n : Wnat_rect P H0 HS (WS n) = HS n (Wnat_rect P H0 HS n). unfold Wnat_rect; simpl. replace (fun_ext unit (W Anat Bnat) (fun _ : unit => n) (fun _ : unit => n) (fun x : unit => match x with | tt => eq_refl end)) with (eq_refl (fun _:unit => n)). reflexivity. admit. Abort. (* However, using tricks and theorems coming from Homotopy Type Theory, we can go further. Assuming functional extensionality for *dependent* products, we can finish the proof. *) Axiom dfun_ext : forall A B (f g:forall x:A,B x), (forall x, f x = g x) -> f = g. Definition f_app {A} {B:A->Type} {f g:forall x, B x} (e:f=g) x : f x = g x := f_equal (fun f => f x) e. (* First we proving dependent functional extensional, but this one will be the inverse of f_app above (see dfun_ext_eqv) *) Definition dfun_ext' {A B}{f g:forall x:A,B x} (e:forall x, f x = g x) : f=g := eq_trans (eq_sym (dfun_ext _ _ _ _ (f_app eq_refl))) (dfun_ext _ _ _ _ e). Definition dfun_ext_eqv {A B} {f g:forall x:A,B x} (w:f=g) : dfun_ext' (f_app w) = w. destruct w. unfold dfun_ext'. destruct (dfun_ext _ _ _ _ (f_app eq_refl)); reflexivity. Qed. Definition Wnat_rect' (P:Wnat->Type) (H0 : P W0) (HS : forall n, P n -> P (WS n)) (n:Wnat) : P n. induction n. destruct a. (* The conclusion is not of the form WS n, because w may not be of the form (fun _ => ..) *) replace w with (fun _:unit => w tt). (* ...but is provably equal to a term of that form *) apply HS. apply (X tt). apply dfun_ext'; intros x. destruct x; reflexivity. replace w with (fun i:False => False_rect Wnat i). apply H0. apply dfun_ext'; intros x. contradiction. Defined. Lemma Wnat_rect_eq0 P H0 HS : Wnat_rect' P H0 HS W0 = H0. unfold Wnat_rect'; simpl. replace (@dfun_ext' False (fun _ : False => Wnat) (fun i : False => False_rect Wnat i) (fun i : False => False_rect (W bool Bnat) i) (fun x => False_ind (False_rect Wnat x = False_rect (W bool Bnat) x) x)) with (eq_refl (fun i => False_rect Wnat i)). reflexivity. rewrite <- dfun_ext_eqv with (w:=eq_refl (fun i => False_rect Wnat i)). f_equal. apply dfun_ext; intros. contradiction. Qed. Lemma Wnat_rect_eqS P H0 HS n : Wnat_rect' P H0 HS (WS n) = HS n (Wnat_rect' P H0 HS n). unfold Wnat_rect'; simpl. replace (@dfun_ext' unit (fun _ => W Anat Bnat) (fun _ : unit => n) (fun _ : unit => n) (fun x : unit => match x with | tt => eq_refl end)) with (eq_refl (fun _:unit => n)). reflexivity. rewrite <- dfun_ext_eqv with (w:=eq_refl (fun _:unit => n)). f_equal. apply dfun_ext; intros. destruct x; reflexivity. Qed. (* But now the above computation rules are "propositional" (i.e. we can replace one side by the other using rewriting), yet both handsides are not convertible *)