The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Another update--I realized if I change "Tactics.change_concl test_term" with "Equality.replace concl test_term", I get a tactic that executes but produces a second goal to prove the equality of the terms.  It would be nice to automatically "admit" the second goal.

                    - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Kenneth Roe <kendroe AT hotmail.com>
Sent: Tuesday, October 3, 2017 6:00 AM
To: Coq-Club
Subject: Re: [Coq-Club] Creating a tactic that changes a conclusion

 

Actually, I realized there is a slight error in the code.  I changed it to:

let test_nat = lazy (Lib_coq.init_constant ["Coq" ; "Init"; "Datatypes"] "nat")

let test_eq = lazy (Lib_coq.init_constant ["Coq";"Init";"Logic"] "eq")

let test_term = Term.mkApp (Lazy.force test_eq, [|(Lazy.force test_nat);Lib_coq.Nat.of_int 2;Lib_coq.Nat.of_int 3|])

(* Top-level arewrite functionality *)

let arewrite : unit Proofview.tactic =

  Proofview.Goal.enter (fun gl ->

  let concl = Proofview.Goal.raw_concl gl in

  let (evm, env) = Lemmas.get_current_context() in

  (*let (body, _) = Constrintern.interp_constr env evm concl in*)

  let _ = print "******* BEGIN *******" in

  let ast = apply_to_definition build_ast env 0 test_term in

  let _ = print ast in

  let _ = print "******* MIDDLE *******" in

  let ast = apply_to_definition build_ast env 0 concl in

  let _ = print ast in

  let _ = print "******* END *******" in

  (print_string "This is a test";

   (*Tacticals.New.tclFAIL 1

    (Pp.str "The tactic is not imlplemented.")*)

          Tacticals.New.tclTHENLIST

            [

              (** Our list of tactics consists in the following single

                  tactic, that changes the conclusion of the goal to

                  [concl'] if [concl] and [concl'] are convertible.

                  (see [tactics/tactis.mli] for other tactics.)  *)

              Tactics.change_concl test_term ;

            ]))

end

However, now I get the error message, "Error: Not convertible.".

                    - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Kenneth Roe <kendroe AT hotmail.com>
Sent: Tuesday, October 3, 2017 5:46 AM
To: Coq-Club
Subject: [Coq-Club] Creating a tactic that changes a conclusion

 

I am trying to create a tactic "arewrite" that will change the conclusion of a goal.

For example, if I have the state:

  a, b, c : nat

  ============================

  eval (c :: (b :: a :: nil)%list)

    (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1)) <=

  eval (c :: (b :: a :: nil)%list) (a_var 2)

Apply "arewrite" should yield the state:

  a, b, c : nat

  ============================

  2=3

I am trying to do this with the code below.

let test_eq = lazy (Lib_coq.init_constant ["Coq";"Init";"Logic"] "eq")

let test_term = Term.mkApp (Lazy.force test_eq, [|Lib_coq.Nat.of_int 2;Lib_coq.Nat.of_int 3|])

(* Top-level arewrite functionality *)

let arewrite : unit Proofview.tactic =

  Proofview.Goal.enter (fun gl ->

  let concl = Proofview.Goal.raw_concl gl in

  let (evm, env) = Lemmas.get_current_context() in

  (*let (body, _) = Constrintern.interp_constr env evm concl in*)

  let _ = print "******* BEGIN *******" in

  let ast = apply_to_definition build_ast env 0 test_term in

  let _ = print ast in

  let _ = print "******* MIDDLE *******" in

  let ast = apply_to_definition build_ast env 0 concl in

  let _ = print ast in

  let _ = print "******* END *******" in

  (print_string "This is a test";

   (*Tacticals.New.tclFAIL 1

    (Pp.str "The tactic is not imlplemented.")*)

          Tacticals.New.tclTHENLIST

            [

              (** Our list of tactics consists in the following single

                  tactic, that changes the conclusion of the goal to

                  [concl'] if [concl] and [concl'] are convertible.

                  (see [tactics/tactis.mli] for other tactics.)  *)

              Tactics.change_concl test_term ;

            ]))

end

However, when I apply the tactic, I get "Error: Not a type.".  What do I need to change?

                          - Ken