The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, May 05, 2012 04:04:03 AM Robbert Krebbers wrote:
> Hello,
> 
> I just ported Herman's Lego formalization [1] to Coq. Together with the
> Type-in-Type patch [2], this gives a nice proof of False.

I actually found http://code.haskell.org/Agda/test/succeed/Hurkens.agda in ;
the 
meantime and eventually managed to translate that into Coq terms, once I 
finally figured out the Agda notation...

Lemma Hurkens : False.
Proof.
set (P := fun A:Type => A -> Prop).
set (U := forall X:Type, (P (P X) -> X) -> P (P X)).
set (τ := fun t:P (P U) =>
  (fun X f p => t (fun x => p (f (x X f)))) : U).
set (σ := fun s:U => s U τ).
set (Δ := (fun y => notT
  (forall p:P U, σ y p -> p (τ (σ y)))) : P U).
set (Ω := τ (fun p => forall x:U, σ x p -> p x) : U).
set (D := forall p:P U, σ Ω p -> p (τ (σ Ω))).
assert (forall p:P U, (forall x:U, σ x p -> p x) -> p Ω)
  as lem1.
exact (fun p H1 => H1 Ω (fun x => H1 (τ (σ x)))).
assert (notT D) as lem2.
exact (lem1 Δ (fun x H2 H3 => H3 Δ H2
  (fun p => H3 (fun y => p (τ (σ y)))))).
assert D as lem3.
exact (fun p => lem1 (fun y => p (τ (σ y)))).
exact (lem2 lem3).
Show Proof.
Defined.

On the other hand, I wouldn't be surprised if by converting my inductive 
types 
to non-inductives, it could be simplified to something similar.  For example:

Definition V :=
  forall P:Type, (forall X:Type, X -> P) -> P.
(* Unsure if this is the right definition... *)
Definition V_const {X:Type} (f:X->V) : V :=
  fun P g => g (X->P) (fun x:X => f x P g).
Definition V_Acc (v:V) : Prop :=
  forall P:V->Prop, (forall (X:Type) (f:X->V),
    (forall x:X, P (f x)) -> P (V_const f)) -> P v.
...

I've also been playing around with the idea of adding dependent types to try 
to produce a short translation of the non-terminating term from untyped 
lambda 
calculus, (λ f . f f) (λ f . f f).  But I haven't been successful in getting 
that one to work out...
-- 
Daniel Schepler

...