4
$\begingroup$

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the change tactic (which can be cumbersome at times), and to make a lemma saying that the two things are equal and then using rewrite. However, the second approach can run into trouble with dependent types, as this example shows:

Definition a := O.

Theorem aO : a = O.
Proof.
  reflexivity.
Qed.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  rewrite aO. (* fails *)
Abort.

So, my question is, is there a way to do something like rewrite but that works in this situation? Of course, I could use change (which is what I currently do), but sometimes the terms being converted are quite large and I would rather not have to type them out.

Edit: Since I've now received two answers that aren't what I'm looking for I thought I would clarify this: I'm not talking about simple situations like in the example where it's just a single definition. I only provided the example to clarify what the fundamental issue is. What I'm asking is, given arbitrary, complicated terms A and B such that change A with B works, how can I get around having to write out A and B every time? Without dependent types I can just use a theorem A = B but I don't know of a way to do it with dependent types.

Improve this question
$\endgroup$
5
  • $\begingroup$ What about simpl? $\endgroup$ Commented Mar 23, 2023 at 9:18
  • $\begingroup$ Also, does rewrite aO in * work, if this extra lemma is acceptable? $\endgroup$ Commented Mar 23, 2023 at 9:20
  • 1
    $\begingroup$ Just a remark, but maybe you know this already: you do not always need to spell out the source of change in full: you only need to give a pattern that matches what you want to change in the target. $\endgroup$ Commented Mar 23, 2023 at 9:57
  • $\begingroup$ @mudri: simpl can only do certain conversions, and it sometimes does too much or too little. rewrite aO in * doesn't work at all (Coq just says "nothing to rewrite"). $\endgroup$ Commented Mar 23, 2023 at 17:42
  • $\begingroup$ If you are looking for complicated change A with B see this example github.com/mukeshtiwari/CoqUtil/blob/main/src/Domain.v $\endgroup$ Commented Jan 31 at 15:38

4 Answers 4

Reset to default
1
$\begingroup$

This works:

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  change a with O.
Abort.

Is this what you need? See the docs. It might be better if you say exactly when you find change cumbersome in the question.

Improve this answer
$\endgroup$
6
  • $\begingroup$ I already mentioned this in the last paragraph of my question: sometimes the terms being converted are quite large and I would rather not have to type them out. $\endgroup$ Commented Mar 23, 2023 at 5:00
  • $\begingroup$ @sudgy So it would not be a Definition, but some arbitrary term in need of changing to some other arbitrary term, right? I don't see how you could provide these two terms apart from writing them out... I mean, how should Coq figure out which two terms to rewrite, if you don't write them out, at least somewhere? $\endgroup$ Commented Mar 23, 2023 at 5:24
  • $\begingroup$ rewrite with a separate theorem figures it out what I want to do just fine. It just doesn't work with dependent types. $\endgroup$ Commented Mar 23, 2023 at 6:17
  • $\begingroup$ @sudgy But you still need to write out what you want to rewrite for rewrite as a theorem. So do you mean you want the ability for Coq to correctly instantiate a theorem for you? $\endgroup$ Commented Mar 23, 2023 at 8:05
  • 1
    $\begingroup$ I feel like my real life examples are way too complicated to describe easily here (you can try searching through github.com/sudgy/math-from-nothing but honestly I would advise against it). I'm fine with writing complicated things out in the statement of a theorem manually. I just don't like huge changes in the middle of a proof. $\endgroup$ Commented Mar 23, 2023 at 17:39
1
$\begingroup$

If you have ssreflect:

Definition a := O.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  rewrite /a.
  rewrite -/a.

If you don't have ssreflect:

Definition a := O.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  unfold a.
  fold a.

Sometimes you have to type the terms out. In this case, use (for example) rewrite -[O]/a.

Improve this answer
$\endgroup$
2
  • $\begingroup$ This doesn't work when the thing you are trying to change is not just a simple definition. $\endgroup$ Commented Mar 23, 2023 at 6:27
  • $\begingroup$ As mentioned in the other answer, if you have complicated expressions which aren't simple definitions, there's no way for Coq to guess which expression you want to change into which other expression, so you'll have to specify the expressions regardless. The "rewrite -[a]/b" syntax works whenever you specify the expressions. $\endgroup$ Commented Mar 25, 2023 at 23:24
1
$\begingroup$

Maybe I should have thought of this more before asking, but I thought of a solution that's at least better than everything I've thought of so far:

Definition a := O.

Theorem aO : a = O.
Proof.
  reflexivity.
Qed.

Ltac def_rewrite H := match type of H with | ?a = ?b => change a with b end.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  def_rewrite aO.
Abort.

However, this solution is not quite as versatile as rewrite is because rewrite can take theorems with parameters and work them out whereas def_rewrite has to take in a theorem with just the form a = b. I'll wait to accept this as the answer in case anybody else can think of a better solution.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Not an answer but it seems likely to extend this using ltac: apply the theorem to evars, (optionally, unify the LHS against arbitrary subterms using match goal and context), then change with the RHS. $\endgroup$ Commented Mar 24, 2023 at 12:47
  • $\begingroup$ @Blaisorblade I'm not that great with ltac, could you expand on that? $\endgroup$ Commented Mar 24, 2023 at 17:45
0
$\begingroup$

Below is one solution but it hinges on proof irrelevance which you may not like. The idea is to generalise the goal ex_intro P 0 Ha = ex_intro P a Ha and turn it into ex_intro P a Ha = ex_intro P b Hb and that is what set (fn :=fun a (H : P a) => ex_intro P a H) is doing.

Require Import Coq.Logic.ProofIrrelevance. 
Definition a := 0.

Theorem aO : a = 0.
Proof.
  reflexivity.
Qed.

Theorem test : forall (P : nat -> Prop) (H : P 0), ex_intro P 0 H = ex_intro P a H.
Proof.
  intros P Ha.
  (* you need to generalise this goal *)
  set (fn := fun a (H : P a) => ex_intro P a H).
  enough (forall u v Hb Hc, u = v -> fn u Hb = fn v Hc) as Hd.
  eapply Hd; eapply eq_sym, aO.
  intros * Hd; subst.
  f_equal.
  eapply proof_irrelevance.
Qed.

If you want to use rewrite

Theorem test : forall (P : nat -> Prop) (H : P 0), ex_intro P 0 H = ex_intro P a H.
Proof.
  intros P Ha.
  (* you need to generalise this goal *)
  set (fn := fun a (Hb : P a) => ex_intro P a Hb).
  enough (forall u v Hb Hc, u = v -> fn u Hb = fn v Hc) as Hd.
  eapply Hd; eapply eq_sym, aO.
  intros * Hd. 
  (* move Ha : P u and Hc : P v back again into the goal to 
   make it more general *)
  revert Hb Hc. 
  rewrite Hd. intros *.
  eapply proof_irrelevance.
Qed.

Btw, your theorem has a simple proof.

Theorem test : forall (P : nat -> Prop) (H : P 0), ex_intro P 0 H = ex_intro P a H.
Proof.
  intros P Ha.
  f_equal.
Qed.
Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.