1
$\begingroup$

When I try to apply a lemma or constructor in Coq, I often run into the situation where lemma doesn't unify exactly with goal I'm working on, even though I know it could be rewritten to match. For example:

Inductive parity :=
| Odd
| Even
.

Inductive has_parity: nat -> parity -> Prop :=
| ZeroEven: has_parity O Even
| SuccOdd n: has_parity n Even -> has_parity (S n) Odd
| SuccEven n: has_parity n Odd -> has_parity (S n) Even
.

(* Not true, but just to show the idea. *)
Lemma example: forall n, has_parity n Even.
Proof.
  intros.
  apply SuccEven.

I get the error:

Error: In environment
n : nat
Unable to unify "has_parity (S ?M150) Even" with "has_parity n Even".

I would like instead for this to succeed, and generate a new goal unifying S ?M150 with n, so I get something like this for the new proof state:

n: nat

-----
Goal 1:
n = S n'

Goal 2:
has_parity n' Odd

It seems that this must be a very common situation, so I would guess that either there is already a solution for this, or there's a good reason that this is not possible.

I am aware that the constructors could be rewritten to create the equalities instead, but I'd like to avoid that if possible.

Ultimately, the question is: Is there already a generic way to do this? If not, can one be made with Ltac/Ltac2? If not, why not?

Edit: Alternative Presentation

I have two inductive propositions, and they are demonstrably equivalent.

Definition f (n: nat): nat.
Proof.
Admitted.

Inductive example_eq: nat -> Prop :=
| case_eq n m: m = (f n) -> example_eq m
.

Inductive example_direct: nat -> Prop :=
| case_direct n: example_direct (f n)
.

Lemma examples_equivalent: forall n, example_eq n <-> example_direct n.
Proof.
  intros.
  split; intro H; inversion H; subst; econstructor; reflexivity.
Qed.

The difference between these two examples is that in example_eq, rather than saying example_eq (f n), we say that example_eq m if m = f n.

My goal is to have a tactic my_apply where, when I write my_apply case_direct, it acts more-or-less as if I had written case_direct like case_eq.

More concretely, considering this proof:

Lemma try_it_direct: forall n, example_direct n.
Proof.
  intros.
  eapply case_direct.

The proof fails with the error Unable to unify "example_direct (f ?M150)" with "example_direct n".

On the other hand, example_eq can handle the eapply:

Lemma try_it_eq: forall n, example_eq n.
Proof.
  intros.
  eapply case_eq.

The proof state is now:

n: nat
========================
n = f ?n

I would like the tactic my_apply to work something like this:

Lemma try_it_direct: forall n, example_direct n.
Proof.
  intros.
  my_apply case_direct.

Proof state:

n: nat
========================
n = f ?n

Real-world example

This question stems from this comment in the autosubst library, where the author opted to use the example_eq strategy.

$\endgroup$
2
  • $\begingroup$ I may expand this into a full answer later, but the short answer to "Ultimately, the question is: Is there already a generic way to do this?" is "not in the standard library or any library I'm aware of, though it might exist somewhere" and the answer to "If not, can one be made with Ltac/Ltac2?" is "yes but it requires recursing under binders which is a doable but painful". There's also the question of whether you want to treat dependent and independent arguments separately. $\endgroup$ Commented Jan 2 at 15:24
  • $\begingroup$ It seems the applys_eq tactic from LibTactics corresponds to what you want? $\endgroup$ Commented Jun 17 at 12:06

2 Answers 2

0
$\begingroup$

I often run into the situation where lemma doesn't unify exactly with goal I'm working on

In the first example you have presented, you would usually just do induction on n, which, given the definition of nat, would give you two sub-goals to solve: one for the case n is O, and one for the case n is an S n', which indeed correspond to the "equations" you were looking for. By the way, destruct n already would do that, additionally with induction you get the inductive hypotheses.

More generally (but I hope I am not simplifying too much), when a statement depends on the specific structure of an otherwise arbitrary term, the proof of the statement will have to proceed by case analysis, i.e. by destructing (up to induction) on the structure of the term (whether directly or indirectly via some lemma or tactic). -- Indeed, for an analogy, there is no such thing as only considering some specific instantiations of a term, just as there is no such thing as partial pattern matching in a total programming language such as Coq/Gallina.

Unable to unify "has_parity (S ?M150) Even" with "has_parity n Even".

The former is (the form of) the conclusion in SuccEven, the latter is (the form of) the conclusion in the goal as per your proof state at that point, and the two simply cannot be unified, since the n in the goal's conclusion is an arbitrary nat, i.e. not necessarily of the form S n' as in the conclusion of SuccEven.

A bit more technically, that ?M150 represents an existential variable: if you have Prolog unification in mind, that is akin to a "logical variable", while n in that sense is a "ground term", and s(M150) = n indeed fails in Prolog, too...

This question stems from this comment in the autosubst library, where the author opted to use the example_eq strategy.

Here is some code for a direct comparison. (Working with "logical variables" I find intriguing, but I have not yet done much in that sense. Anyway, given there is a cost-benefit involved, I suppose whether to use one approach vs the other boils down to what is more convenient relative to the specific needs and preferences one has...)

(** Some inductive "predicate". *)
Inductive dir : nat -> Prop :=
| Dir n : dir (S n).

(** Lemma to "extract equations" from a
    *conclusion* of the form [dir m].
    Notice we need an *existential* assumption,
    and a forward-reasoning [destruct]. *)
Lemma dir_from_eqns : forall m,
  (exists n, m = S n) -> dir m.
Proof.
  intros m E.
  destruct E as [n H].
  rewrite H.
  constructor.
Qed.

(** Example e-application from "extraction". *)
Example ex_dir_from_eqns : forall n,
  dir (S (S n)).
Proof.
  intros n.
  apply dir_from_eqns.
  econstructor.
  reflexivity.
Qed.

(** For comparison: ******** *)

(** Definition with "equations". *)
Inductive dir' : nat -> Prop :=
| Dir' n m : m = S n -> dir' m.

(** Example e-application is more direct... *)
Example ex_dir'_from_eqns : forall n,
  dir' (S (S n)).
Proof.
  intros n.
  econstructor.
  reflexivity.
Qed.

(** On the other hand, [dir] is simpler... *)
Example ex_dir_is_simpler : forall n,
  dir (S (S n)).
Proof.
  intros n.
  constructor.
Qed.

(** For sanity of the comparison: ******** *)

(** Our definitions are equivalent. *)
Lemma dir'_equiv_dir : forall n,
  dir' n <-> dir n.
Proof.
  intros n.
  split; intros H.
  - (* -> *)
    inversion H; subst.
    constructor.
  - (* <- *)
    inversion H; subst.
    econstructor.
    reflexivity.
Qed.
$\endgroup$
10
  • $\begingroup$ I'm not really looking to solve the example; it was just to demonstrate the issue. In the real proof I'm working on, the cases of the Inductive are more like MyCase: SomeH -> MyInductive (f x) for some function f. What I want to do is have a tactic which would treat that case as if it had said MyCase: f x = y -> SomeH -> MyInductive y. $\endgroup$
    – Matt
    Commented Dec 23, 2023 at 23:46
  • $\begingroup$ Especially since we cannot do much with a false theorem anyway: in that sense, a theorem that can be proven indeed is already a better example to play with. That said, even with that 'MyCase', nothing changes re what I have explained above: if you have something like unification in Prolog in mind, then notice that these "x", "y", or "n" are not logical variables, these are akin to ground terms in that sense, a logical variable is the "?M150" in your question... $\endgroup$ Commented Dec 24, 2023 at 11:24
  • $\begingroup$ @Matt Meanwhile I have tried and expanded my answer: I hope that makes it clearer, but please feel free to tell if there is still something unclear/lacking. $\endgroup$ Commented Dec 24, 2023 at 12:39
  • $\begingroup$ I've edited the original question to add some more detail. I still don't have a correct theorem to work with, but hopefully my goal is a little clearer. $\endgroup$
    – Matt
    Commented Dec 26, 2023 at 23:22
  • $\begingroup$ @Matt Thanks for that last link, that indeed clarifies the question to me. But I just cannot see a substantial difference between the two styles of definition (might be me). Indeed, I have played with your latest code and, however I approach it, I keep getting back to the same place... -- I am going to add some code. $\endgroup$ Commented Dec 27, 2023 at 14:17
0
$\begingroup$

I've come up with the following Ltac2 code. It works for my purposes.

From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Message.
From Ltac2 Require Import Constr.

Ltac2 rec concl_aux a := lazy_match! a with
| ?b -> ?c => concl_aux c
| _ => a
end.

Ltac2 concl h := let a := (type h) in concl_aux a.

Ltac2 mapply h := 
    let g := Control.goal () in
    let c := concl h in
    let h' := Fresh.in_goal @H in
    Std.assert (Std.AssertType (Some (Std.IntroNaming (Std.IntroFresh h'))) constr:($g = $c) None);
    Control.dispatch [
        (fun _ => ltac1:(f_equal));
        (fun _ => (
            ltac1:(h' |- rewrite h') (Ltac1.of_ident h');
            Std.apply false false [fun _ => h, Std.NoBindings] None
        ))
    ].

Ltac2 Notation "mapply" h(constr) := mapply h.
```
$\endgroup$
1
  • $\begingroup$ I don't know Ltac2 so I cannot judge the quality of your solution, but I must applaud you for doing what I eventually didn't have the courage of doing. ;) I'd suggest you add some example usage, to show how/that it works, then (modulo any intervening objections) you could just accept your solution as an answer. $\endgroup$ Commented Jan 17 at 12:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.