The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

Abuse of coercions gives weird results in coqtop.

$ coqtop
Welcome to Coq 8.2pl1 (February 2010)
Coq < Unset Printing All.
Coq < Require Import fib13.
Ambiguous paths:
[fib13.expr2] : fib13.type >-> Sortclass
Coq < Check a1.
a1
     : FUCKMS
Coq < Check a2.
a2
     : FUCKMS -> False
Coq < Print Assumptions a1.
Closed under the global context
Coq < Print Assumptions a2.
Closed under the global context
Coq < Print False.
Inductive False : Prop :=

I have problem getting a real contradiction though.

Attached is source code.

-- 
joro
(* Part of this file is from 
http://www-verimag.imag.fr/~boulme/SIMPLY_TYPED_LAMBDA_MU/SimplyTypedLambdaMu.v
 *)

(** * Mixed Embedding of Simply Typed Lambda-Mu Calculus. 

  This file is an introduction to the simply typed version of 
  Parigot's calculus. It implements Curry-Howard paradigm in 
  classical propositional logic.

  I prove here that the logic is consistent. 
  I also give a weak result on the completeness of the proof system.
  I emulate in Coq an interpreter of this lambda-calculus
  (I give small examples of reduction). 

  Technically, I use a higher-order abstract syntax technique to
  avoid the tedious handling of binders.
  
 *)


Set Implicit Arguments.

(** Preliminary: negation on Type *)

Definition neg (A: Type) := A -> False.


(** * Syntax of types (e.g. of classical propositions).

  We consider here Coq propositions as atomic formulas. 
 *)
Inductive type: Type :=
  | ATOM: Prop -> type
  | ARROW: type -> type -> type.

Infix "==>" := ARROW (at level 80, right associativity).

(** * Derived types *)

Definition FUCKMS: type := ATOM False.

Definition TRUE: type := ATOM True.

Definition NOT (T: type): type 
  := T ==> FUCKMS.

Definition OR (A B: type): type
  := (NOT A) ==> B.

Definition AND (A B: type): type
  := NOT (A ==> (NOT B)).

(** * Syntax of Terms (e.g. of proofs) *)

Section TERMS.

(** I give the abstract syntax of terms before to explain there
  informal meaning (see "logical intuitions" below). The calculus is a 
  usual lambda-calculus extend with a continuation-handling mechanism.
  - In order to avoid the encoding of variable substitution, 
    a bound variable is represented directly as a Coq function
    (see [LAMBDA] and [MU] binders).
  - Terms are parameterized by the (meta)type of variables.
  - Here, we represent only "well-typed" terms (typing of lambda-mu
  calculus is emulated by Coq typing).
  - The meta-type of variables is itself parameterized by a type
    (the type of term abstracted by the given variable).
  - In this language, there are two syntactic categories of variable:
  -- [vV] (variable for "values") introduced by [LAMBDA].
  -- [vC] (variable for "continuations") introduced by [MU].
 *)
Variable vV: type -> Type.
Variable vC: type -> Type.

Inductive term: type -> Type :=
  (** usual constants: we embed here double negation of Coq proofs *)
  | CTE (P:Prop): neg (neg P) -> (term (ATOM P))
  (** usual variables *)
  | VAR (A:type): (vV A) -> (term A)
  (** usual lambda-abstraction  *)
  | LAMBDA (A B:type): ((vV A) -> (term B)) -> (term (A ==> B))
  (** usual application *)
  | APP (A B:type): (term (A ==> B)) -> (term A) -> (term B)
  (** application of a term to a continuation (branch to this continuation) *)
  | BRA (A:type): (vC A) -> (term A) -> (term FUCKMS)
  (** abstraction of a continuation *)
  | MU (A:type): ((vC A) -> (term FUCKMS)) -> (term A)