search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

Why does hammer succeed if it's not suppose to call induction? #124

Closed brando90 closed 2 years ago

brando90 commented 2 years ago

See:

  From Hammer Require Import Hammer.

  Theorem n_plus_0_eq_n:
  forall n:nat,
    n + 0 = n.
  Proof.
  by hammer.
  Qed.

proof is closed without me requiring to call induction n ...

brando90 commented 2 years ago

likely works due to using these lemmas:

Coq.Init.Datatypes.nat, Coq.Init.Datatypes.O, Coq.Init.Nat.add, Coq.Init.Peano.plus_O_n, Coq.Arith.PeanoNat.Nat.add_0_l

available for preed. Saw them with predict 5.

brando90 commented 2 years ago

actually this also succeds with sauto :/

  From Hammer Require Import Hammer.

  Theorem n_plus_0_eq_n:
  forall n:nat,
    n + 0 = n.
  Proof.
  by sauto.
  Qed.

which docs imply sauto doesn't do dependency selection...

lukaszcz commented 2 years ago

But it does arithmetic. See the "lia:" option.