Stack Overflow
Stack Overflow

Questions tagged [ltac]

The Ltac language, Coq's domain-specific language for proof search procedures. Use this tag on questions about the language and questions about proof automation using Ltac.

Here are some references on Ltac:

  • The Coq Reference Manual, sect. 9;
  • Certified Programming with Dependent Types by A. Chlipala, the Proof Search in Ltac chapter;
  • The original paper: A Tactic Language for the System Coq by D. Delahaye (‎2000).
72 questions
9
votes
2 answers

Extensible tactic in Coq

Let’s say I have a fancy tactic that solves lemmas of a certain kind: Ltac solveFancy := some_preparation; repeat (first [important_step1 | important_step2]; some_cleanup); solve_basecase. Now I use this tactic to prove further…
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
8
votes
1 answer

How do I write tactics that behave like "destruct ... as"?

In coq, the destruct tactic has a variant accepting an "conjunctive disjunctive introduction pattern" that allows the user to assign names to introduced variables, even when unpacking complex inductive types. The Ltac language in coq allows the user…
phs
  • 10,687
  • 4
  • 58
  • 84
8
votes
1 answer

Coq: Ltac definitions over variable argument lists?

While trying to create an Ltac definition that loops over a variable-length argument list, I encountered the following unexpected behavior on Coq 8.4pl2. Can anyone explain it to me? Ltac ltac_loop X := match X with | 0 => idtac "done" | _ =>…
Kevin Hamlen
  • 185
  • 3
7
votes
1 answer

How to match a "match" expression?

I am trying to write a rule for hypotheses, formulated with a help of match construction: Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat. intros. x : nat H : match x with | 0%nat => 10%nat | 1%nat => 5%nat | S…
Necto
  • 2,594
  • 1
  • 20
  • 45
6
votes
2 answers

Raising the failure level of a coq tactic

When implementing a complex tactic in Ltac, there are some Ltac commands or tactic invocation that I expect to fail and where that is expected (e.g. to terminate a repeat, or to cause backtracking). These failures are usually raised at failure level…
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
6
votes
1 answer

Ltac : optional arguments tactic

I want to make a Ltac tactic in coq which would take either 1 or 3 arguments. I have read about ltac_No_arg in the LibTactics module but if I understood it correctly I would have to invoke my tactic with : Coq < mytactic arg_1 ltac_no_arg…
L. Soret
  • 169
  • 10
5
votes
1 answer

Coq forward reasoning: apply with multiple hypotheses

I have two hypothesis, and I would like to use forward reasoning to apply a theorem that uses both of them. My specific I have the hypothes H0 : a + b = c + d H1 : e + f = g + h and I want to apply the theorem from the standard…
Jeremy Salwen
  • 8,061
  • 5
  • 50
  • 73
5
votes
1 answer

How to look at multiple goals at the same time?

I am considering writing tactics which will look at multiple goals and make decision based on that. However, when I use match goal with and stare at a goal, how do I say "please find another goal that looks like this"? Or rather, a more general…
Jason Hu
  • 6,239
  • 1
  • 20
  • 41
5
votes
1 answer

Matching with Ltac on a call containing local variable

I have a goal that contains a call to some lemma foo within branch of a match. That call uses as one of its arguments a variable R local to the branch: | SomeConstr => fun R => .... (foo a b c R) .... I would like to perform beta expansion on foo…
Jan Stolarek
  • 1,409
  • 1
  • 11
  • 21
5
votes
1 answer

Tactics with variable arity

Say I want to have a tactic to clear multiple hypothesis at once, to do something like clear_multiple H1, H2, H3.. I tried to do that using pairs, like the following: Ltac clear_multiple arg := match arg with | (?f, ?s) => clear s; clear_multiple…
Bromind
  • 1,065
  • 8
  • 23
5
votes
3 answers

rewrite single occurence in ltac

How can I invoke rewrite in ltac to only rewrite one occurrence? I think coq's documentation mentions something about rewrite at but I haven't been able to actually use it in practice and there are no examples. This is an example of what I am trying…
Mei Zhang
  • 1,434
  • 13
  • 29
4
votes
1 answer

Modus Ponens and Modus Tollens in Coq

I would like to have Ltac tactics for these simple inference rules. In Modus Ponens, if I have H:P->Qand H1:P, Ltac mp H H1 will add Qto the context as H2 : Q. In Modus Tollens, if I have H:P->Qand H1:~Q, then Ltac mt H H1 will add H2:~Pto the…
mlg556
  • 419
  • 3
  • 13
4
votes
3 answers

Coq: viewing proof term during proof script writing

So, I've got a proof that looks like this: induction t; intros; inversion H ; crush. It solves all my goals, but when I do Qed, I get the following error: Cannot guess decreasing argument of fix. So somewhere in the generated proof term, there's…
jmite
  • 8,171
  • 6
  • 40
  • 81
4
votes
1 answer

How to do "negative" match in Ltac?

I want to apply a rule in a case when some hypothesis present, and another is not. How can I check for this condition? For example: Variable X Y : Prop. Axiom A: X -> Y. Axiom B: X -> Z. Ltac more_detail := match goal with |[H1:X,
Necto
  • 2,594
  • 1
  • 20
  • 45
4
votes
1 answer

Coq: "dependent induction" inside Ltac

Dependent induction seems to work differently for me in an Ltac and not. The following works just fine: Require Import Coq.Program.Equality. Goal forall (x:unit) (y:unit), x = y. intros. dependent induction x. dependent induction…
jbapple
  • 3,297
  • 1
  • 24
  • 38
1
2 3 4 5