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 *)