The Coq mailing list

[Elias Castegren <eliasca AT kth.se>]

Hi Abhishek!

I asked about something similar to this a while back.

After a few changes back and forth, I found that this

simple solution is what works best for me:

```

Require Import QArith QArith.Qcanon Psatz.

Lemma Q2Qc_eq_l :

  forall q,

    Q2Qc q == q.

Proof.

  intros q.

  cbv [this Q2Qc].

  apply Qred_correct.

Qed.

Ltac drop_Q2Qc :=

  match goal with

  | [H : context[Q2Qc] |- _] => setoid_rewrite Q2Qc_eq_l in H

  | [_ : _ |- context[Q2Qc]] => setoid_rewrite Q2Qc_eq_l

  end.

Ltac Qify :=

  unfold Qcminus, Qcplus, Qcopp in *;

  unfold Qclt, Qcle in *;

  repeat drop_Q2Qc.

```

Using `Qify` followed by `lra` solves most simple Qc goals.

Sometimes `drop_Q2Qc` is not able to get rid of all the 

`Q2Qc`s in the context, and I haven’t been able to figure

out why. There might also be other unfolds you will want to

do in `Qify`.

Let me know if you come up with improvements!

Cheers

/Elias

8 jan. 2021 kl. 21:47 skrev Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

I see that there is a field instance for Qc.

Is there a psatz/lra like tactic for Qc?

If not, is there a tactic to preprocess a Qc goal to Q, something like what zify does? (Thanks Frédéric for solving the problem in the other thread.)

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/