The Coq mailing list

[吉川 将司 <os0220 AT hotmail.com>]

Hi!

I want to implement a Coq tactic which consults some

outer resources and declares a new axiom based on those.

This will be useful for proving natural language theorems.

I wrote an OCaml code for this but it does not work as expected.

I'd like to have your help to fix this.

Here's my first attempt (I use Coq v8.6):

theory.v:

  Parameter is_foo : nat -> Prop.

  Definition def1 : Prop := (forall x : nat, is_foo x).

test.ml4:

  DECLARE PLUGIN "test"
  let contrib_name = "test"
  let find_constant contrib dir s =
      Universes.constr_of_global @@ Coqlib.find_reference contrib dir s
  let init_constant dir s = find_constant contrib_name dir s
  let imp = lazy (init_constant ["theory"] "def1")

  let test = Proofview.Goal.nf_enter { enter = begin fun gl ->
      let sigma = Tacmach.New.project gl and env = Tacmach.New.pf_env gl in
      let cexpr = Constrextern.extern_type true env sigma (Lazy.force imp) in
      let loc_ident = (Loc.ghost, Names.Id.of_string "axiom1") in
      let pl = (loc_ident, None) in
      let l = [false, ([pl], cexpr)] in
      let status = Command.do_assumptions (Decl_kinds.Global, false, Decl_kinds.Logical)   Vernacexpr.NoInline l in
      Tacticals.New.tclIDTAC (* put this to end with tactic type *)
  end }

  TACTIC EXTEND _test_
  | [ "test" ] -> [ test ]
  END

******

This fails and leads to an anomaly:

$ coq_makefile test.ml4 -o Makefile; make; coqc theory.v

$ coqtop

Welcome to Coq 8.6 (November 2017)

Coq < Declare ML Module "test".
[Loading ML file test.cmxs ... done]

Coq < Require Export theory.

Coq < Goal forall x, is_foo x.
1 subgoal

  ============================
  forall x : nat, is_foo x

Unnamed_thm < test.
axiom1 is declared
1 subgoal

  ============================
  forall x : nat, is_foo x

Unnamed_thm < apply axiom1.
No more subgoals.

Unnamed_thm < Qed.
test.
(apply axiom1).

Qed.
Toplevel input, characters 0-4:
> Qed.
> ^^^^
Anomaly: Uncaught exception Not_found. Please report at
http://coq.inria.fr/bugs/.

******

However, this new axiom is available for proving other theorems

after exiting from the proof with Admitted.

Unnamed_thm < Admitted.
Unnamed_thm is declared

Coq < Goal forall x, is_foo x.
1 subgoal

  ============================
  forall x : nat, is_foo x

Unnamed_thm0 < apply axiom1.
No more subgoals.

Unnamed_thm0 < Qed.
(apply axiom1).

Qed.
Unnamed_thm0 is defined

******

I suspect the problem relates to Environ.env.

The defined axiom resides on Global.env but not seeable from

the proof session for Unnamed_thm somehow...

Thanks,

Masashi Yoshikawa