The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

MathClasses has something similar, which I like a lot:

http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Feb 25, 2016 at 5:39 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Wed, Feb 24, 2016 at 4:17 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:
> Hi,
>
> I recently discovered the Lean Theorem Prover
> (https://leanprover.github.io/about/). I did some toy experiments with it
> and and, at least in this first contact, it seemed similar to Coq. I am
> curious about how the Coq community sees Lean. Does it see Lean as
> "competitor" of Coq? Is it possible for Coq to bridge the gap betweem
> interactive and automated theorem proving like Lean aims to do?

One thing I did notice in my quick browse through the tutorial: its
standard library includes a typeclass for decision procedures for
propositions (though I'd call it Decision instead of decidable as Lean
does, as the last suggests the proposition (P \/ ~P) rather than
something with extractable information).  It also includes a notation
for defining a proof by inferring a decision procedure and then
running it.

This is something I've thought of proposing as an addition to the Coq
standard library at various times - and I might even have mentioned
some elements of my thinking in some previous messages to the list.
So, the basic outline would be something like:

Class Decision (P:Prop) : Set :=
decide : {P} + {~P}.

Arguments decide P [Decision].

Instance true_dec : Decision True := left _ I.
Instance and_dec {P Q:Prop}
  `{!Decision P} `{!Decision Q} : Decision (P /\ Q) := ...
...
Instance bounded_nat_dec {P : nat -> Prop}
  `{!forall m:nat, Decision (P m)}
  (n : nat) : Decision (forall m:nat, m < n -> P m) :=
fix ...
Instance Forall_dec {A:Type} {P : A -> Type}
  `{!forall x:A, Decision (P x)}
  (l : list A) : Decision (Forall P l) :=
fix ...
...

Ltac decide :=  (* untested *)
match goal with
|- ?P =>
  let dec := hnf (decide P) in
  match dec with
  | left _ ?pf => exact pf
  | right _ _ => error 2 "statement is false"
  | _ => error 2 "could not evaluate decision procedure"
  end
end.
Notation decision_pf := ltac:(decide).

Example my_max (m n:nat) : nat :=
if decide (m <= n) then n else m.

Maybe it could also include some framework for enumerating all
elements of finite types, which would be useful for things like
Definition bor_assoc (x y z:bool) :
  bor x (bor y z) = bor (bor x y) z := decision_pf.
--
Daniel Schepler