I was curious about ATPs within the logic of Coq itself (e.g. that do induction sort of smartly). Do people know of tools better than sauto, coqhammer? (note SMTCoqhammer also uses FOL solvers/atps so I don’t think that’s quite what I’m curious about)
I had a similar discussion (that sort of ended) in Coq hammer’s gitissues: Extending hammer/sauto to use induction? · Issue #125 · lukaszcz/coqhammer · GitHub
I wanted to use a “hammer”
coq_simp_atp. to solve very simple proofs for me. e.g.
have: forall n: my_nat, O [+] n = n [+] O. by coq_simp_atp.
for example currently the above cannot be solved by
by sauto. or
by hammer. since they require induction e.g.
have: forall n: my_nat, O [+] n = n [+] O. induction n. by sauto. by sauto.
is the needed proof. Is there some type of hammer that does this for simple cases in coq?
From Coq Require Import ssreflect ssrfun ssrbool. From Hammer Require Import Tactics Hammer. Inductive my_nat : Type := | O : my_nat | S : my_nat -> my_nat. Fixpoint add_left (n m : my_nat) : my_nat := match n with | O => m | S n' => S (add_left n' m) end. Notation "x [+] y" := (add_left x y) (at level 50, left associativity). Theorem my_add_comm: forall n m : my_nat, n [+] m = m [+] n. Proof. intros. induction n as [| n' IH]. - have: forall n: my_nat, O [+] n = n [+] O. induction n. by sauto. by sauto. by sauto.