Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol).

Damien is critical of "fully certified decision procedure returning wrong results"

My quesion is:

Why should I trust Coq if it proves False?

(If someone mentions results of coqchk, it is a bug by itself to not trust their compiler and in addition coqchk is known to loop forever after minor hex editing .vos).

Here is an session:

  ~/coq-test/bin/coqtop
  Welcome to Coq 8.3pl2 (June 2011)

  Coq < Require Import bug2.
  Coq < Check Omega.
  Omega
      : False
  Coq < Print Assumptions Omega.
  Closed under the global context

(code bug2.v for posterity, author Damien Pous)

    Require List.
    Set Implicit Arguments.
    Implicit Arguments inr [A B].
    Implicit Arguments inl [A B].

    (* a simple signature for maps *)
    Module Type MAP.
     Parameter key: Type.
     Parameter t: Type -> Type.
     Section s.
      Variable A: Type. 
      Parameter empty: t A.
      Parameter add: key -> A -> t A -> t A.
      Parameter find: key -> t A -> option A.
     End s.
     Implicit Arguments empty [[A]].
    End MAP.

    (* maps indexed by natural numbers *)
    Module NMap <: MAP.
     Definition key := nat.
     Section s.
      Variable A: Type.
      Definition t := list (option A).
      Definition empty: t := nil.
      Fixpoint add i v (m: t) :=
        match i,m with
        | O,nil => cons (Some v) nil
        | O,cons _ q => cons (Some v) q
        | S i,nil => cons None (add i v nil)
        | S i,cons o q => cons o (add i v q)
        end.
      Definition find i (m: t) := List.nth i m None.
     End s.
     Implicit Arguments empty [[A]].
    End NMap.

    (* maps indexed by booleans *)
    Module BMap <: MAP.
     Definition key := bool.
     Section s.
      Variable A: Type.  
      Definition t := (option A*option A)%type.
      Definition empty:t := (None,None).
      Definition find (b: bool) (m: t) := if b then fst m else snd m.
      Definition add (b: bool) v (m: t) := let (t,f) := m in if b then (Some v,f) else (t,Some v).
     End s.
     Implicit Arguments empty [[A]].
    End BMap.

    (* maps indexed by unit *)
    Module UMap <: MAP.
     Definition key := unit.
     Section s.
      Variable A: Type.  
      Definition t := option A.
      Definition empty: t := None.
      Definition find (b: unit) (m: t): option A := m.
      Definition add (b: unit) (v: A) (m: t): t := Some v.
     End s.
     Implicit Arguments empty [[A]].
    End UMap.

    (* maps indexed by pairs *)
    Module PairMap(H: MAP)(K: MAP) <: MAP.
     Definition key := prod H.key K.key.
     Section s.
      Variable A: Type.  
      Definition t := H.t (K.t A).
      Definition empty: t := H.empty.
      Definition find xy (m: t) :=
        let '(pair x y) := xy in
          match H.find x m with
          | None => None
          | Some n => K.find y n
          end.
      Definition add xy v (m: t) :=
        let '(pair x y) := xy in
          match H.find x m with
          | None => H.add x (K.add y v K.empty) m
          | Some n => H.add x (K.add y v n) m
          end.
     End s.
     Implicit Arguments empty [[A]].
    End PairMap.

    (* maps indexed by sums *)
    Module SumMap(H: MAP)(K: MAP) <: MAP.
     Definition key := sum H.key K.key.
     Section s.
      Variable A: Type.  
      Definition t := prod (H.t A) (K.t A).
      Definition empty: t := (H.empty, K.empty).
      Definition find s (m: t) :=
        match s with 
          | inl x => H.find x (fst m)
          | inr y => K.find y (snd m)
        end.
      Definition add s v (m: t) :=
        let '(h,k) := m in
        match s with 
          | inl x => (H.add x v h,k)
          | inr y => (h,K.add y v k)
        end.
     End s.
     Implicit Arguments empty [[A]].
    End SumMap.


    (** selecting these lines, we will get a proof of [False] *)
    Module MMap := NMap.
    Definition v := O.

    (** selecting these lines will give a "bus error" rather than a proof of [False] *)
    (* Module MMap := BMap. *)
    (* Definition v := false. *)

    (** selecting these ones will silently kill the coq process instead *)
    (* Module MMap := UMap. *)
    (* Definition v := tt. *)


    (* we need a functor to make the bug appear *)
    Module Make(VMap: MAP).
     (* I didn't manage to get the bug with fewer functor applications *)
     Module TMap := SumMap VMap MMap.
     Module MTMap := PairMap MMap TMap.
     Module MTTMap := PairMap MTMap TMap.
     (* commenting this goal makes the first bug disappear! *)
     Goal MTTMap.find (v,inr v,inr v) (MTTMap.add (v,inr v,inr v) 64 MTTMap.empty) = Some 64.
     Proof. vm_compute. reflexivity. Qed.
    End Make.

    Module Import B := Make UMap.

    (* uncommenting this goal and its proof makes the bug disappear! *)
    (* Goal MTMap.find (v,inr v) *)
    (*   (MTMap.add (v,inl tt) 16 (MTMap.add (v,inr v) 64 MTMap.empty)) <> None. *)
    (* Proof. vm_compute. congruence. Qed. *)

    (* this lemma is ok, and proved with [compute] *)
    Lemma l1: MTTMap.find (v,inr v,inr v) 
      (MTTMap.add (v,inr v,inl tt) 16 (MTTMap.add (v,inr v,inr v) 64 MTTMap.empty)) = Some 64.
    Proof. compute. reflexivity. Qed.

    (* BUG: this lemma is wrong but proved thanks to [vm_compute] *)
    Lemma l2: MTTMap.find (v,inr v,inr v) 
      (MTTMap.add (v,inr v,inl tt) 16 (MTTMap.add (v,inr v,inr v) 64 MTTMap.empty)) = None.
    Proof. vm_compute. reflexivity. Qed.


    (* coqcheck detects that this assumption-free proof of [False] is ill-typed *)
    Theorem Omega: False.
    Proof. generalize l1 l2. congruence. Qed.
    Print Assumptions Omega.



    (* renaming the module for the first call to [add] solves the problem! *)
    Module M := MTTMap.
    Goal MTTMap.find (v,inr v,inr v) 
      (M.add (v,inr v,inl tt) 16 (MTTMap.add (v,inr v,inr v) 64 MTTMap.empty)) <> None.
    Proof. vm_compute. congruence. Qed.




    (* no problemb without the functor [Make] *)
    Module Ok.
     Module TMap := SumMap UMap MMap.
     Module MTMap := PairMap MMap TMap.
     Module MTTMap := PairMap MTMap TMap.
     Goal MTTMap.find (v,inr v,inr v) 
       (MTTMap.add (v,inr v,inl tt) 16 (MTTMap.add (v,inr v,inr v) 64 MTTMap.empty)) = Some 64.
     Proof. vm_compute. reflexivity. Qed.
    End Ok.


    (* Tested with 
        v8.3  -r 14152 and -r 14299
        trunk -r 14299
     *)
share|improve this question
    
What's the question here? Certainly you shouldn't believe everything coq says until this bug has been fixed. –  Noah Snyder Sep 16 '11 at 15:11
    
Appears to have been fixed a month ago? coq.inria.fr/bugs/show_bug.cgi?id=2580 –  Sam Nead Sep 16 '11 at 15:15
1  
See also mathoverflow.net/questions/63816 and tea.mathoverflow.net/discussion/1037 for a discussion of a related question by joro. –  Emil Jeřábek Sep 16 '11 at 15:27
    
@Sam It appears fixed in trunk (which is considered unstable by some) while it doesn't appear fixed in a Coq release version. –  joro Sep 18 '11 at 11:20
add comment

closed as not a real question by Emil Jeřábek, Noah Snyder, Ben Webster Sep 16 '11 at 15:14

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

Browse other questions tagged or ask your own question.