The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Sun, May 29, 2011 at 04:20:40PM +0300, Georgi Guninski wrote:
> On Sun, May 29, 2011 at 04:14:45PM +0300, Georgi Guninski wrote:
> > 
> > I have problem getting a real contradiction though.
> > 
> > Attached is source code.
> >
> 
> something corrupted the attachment.
> the source is at: http://j.ludost.net/blog/misc/fib13.v

my bad, the testcase can be minimized a lot:

Inductive type: Type :=
  ATOM: Prop -> type.
Definition FUCKMS: type := ATOM False.
Definition expr (t:type) : Type := True.
Definition expr2 (t:type) : Type := False.

(** With the following coercion, we embed "type" as a sort of Coq... *)
Coercion expr: type >-> Sortclass.
Coercion expr2: type >-> Sortclass.

Lemma a1: FUCKMS.
Proof.
compute. trivial.
Qed.

Lemma a2: expr2 FUCKMS->False.
Proof.
compute. trivial.
Qed.

(*
can't prove this though...
Lemma aboutfalse: False.
Proof.
pose proof a1.
pose proof a2.
contradict H.
Qed.
*)