The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

Nice version of Russell's paradox.

Two remarks :

- One does not need K nore dependent inversion for the matter.
Just do "case eq" where eq is your equality proof.

- You can simplify your development by noticing right away
that all trees are "good".


Cheers,


Benjamin


(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L16 (Russell's paradox)

    The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section russell.

Set Implicit Arguments.

Variable set : Set.
Variable name : Set -> set.
Variable El : set -> Set.
Axiom reflect : forall A:Set,A = El (name A).

Inductive Tree : Set :=
  span : forall a : set, (El a -> Tree) -> Tree.

Definition elem (t : Tree) (u : Tree) : Prop
  := match u with
     | span A us => exists a : El A , t = us a
     end.

Definition Bad (t : Tree) : Prop
  := elem t t.

Lemma is_good :  forall t, ~Bad t.
induction t; intros [x ex].
unfold not in H; apply (H x).
rewrite <- ex.
exists x; trivial.
Qed.

Definition tree := name Tree.

Definition getTreeAux : forall A : Set, Tree = A -> A -> Tree.
intros A e a; rewrite e; exact a.
Defined.

Definition getAuxTree  : forall A : Set, Tree = A -> Tree -> A.
intros A e a; rewrite <- e; exact a.
Defined.

Definition getTree : El tree -> Tree :=
 fun e => (getTreeAux (reflect _ ) e).

Definition Russell := (span getTree).

Lemma is_bad :  (Bad Russell).
exists (getAuxTree  (reflect _) Russell).
unfold getTree.
case (reflect Tree).
trivial.
Qed.

Definition paradox : False := (is_good _ is_bad).




Le 29 nov. 08 à 15:03, Thorsten Altenkirch a écrit :

> > I suspect I need K (or I am just too stupid). Can anybody conform  
> > either? I.e. can I prove this using Coq.Logic.Eqdep or without?
>
> I am just too stupid. But so is Coq. I just need to use dependent  
> inversion.
>
> Actually I realized that I can prove it with the standard eliminator  
> for equality:
>
> eq_elim : forall (A:Set)(x:A)(P:forall y:A, (x=y)->Set)
>                            (m:P x (refl_equal x))
>                            (y:A)(p:x=y),P y p.
>
> This is not automatically derived by Coq (why not?) but it can be  
> proven using dependent inversion. It seems that you always get in  
> trouble if you try to use dependent types in Coq.
>
> I attach my completed Russell derivation.
>
> Cheers,
> Thorsten
>
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>
> <l16-crib.v>