coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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=
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 conclusionActually, 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 conclusionI 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
- [Coq-Club] Creating a tactic that changes a conclusion, Kenneth Roe, 10/03/2017
- Re: [Coq-Club] Creating a tactic that changes a conclusion, Kenneth Roe, 10/03/2017
- Re: [Coq-Club] Creating a tactic that changes a conclusion, Kenneth Roe, 10/03/2017
- Re: [Coq-Club] Creating a tactic that changes a conclusion, Matthieu Sozeau, 10/03/2017
- Re: [Coq-Club] Creating a tactic that changes a conclusion, Kenneth Roe, 10/03/2017
- Re: [Coq-Club] Creating a tactic that changes a conclusion, Kenneth Roe, 10/03/2017
Archive powered by MHonArc 2.6.18.