Why should I trust Coq when assumption-free proof of False in Coq exists?

2011-09-16T14:54:50Z

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
     *)

Why should I trust Coq when assumption-free proof of False in Coq exists? - MathOverflow [closed]

Why should I trust Coq when assumption-free proof of False in Coq exists?