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