Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Creating a tactic that changes a conclusion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Creating a tactic that changes a conclusion


Chronological Thread 
  • From: Matthieu Sozeau <mattam AT mattam.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Creating a tactic that changes a conclusion
  • Date: Tue, 03 Oct 2017 18:55:16 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
  • Ironport-phdr: 9a23:ngb4MBzTcnSMmAbXCy+O+j09IxM/srCxBDY+r6Qd0u8QIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclZeZzee3rrjafxlIhTegKYh1Phi/sE2Fs8AKnYJnAqM41gfApz1PYesAljAgHk6agxupvpT4x5Vk6SkF4/8=

Hi Kenneth, it seems your goal is an <= while you convert with an equality, hence I'm not sure they are convertible.
-- Matthieu

On Tue, Oct 3, 2017 at 3:20 PM Kenneth Roe <kendroe AT hotmail.com> wrote:
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

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




Archive powered by MHonArc 2.6.18.

Top of Page