The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a tactic that can solve goals like this, in Q or R or Z?  (I haven't managed to get csdp working for psatz, and none of nsatz, lia, nia, nra, lra, fourier, field, ring, omega seem to work):

Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.nsatz.Nsatz Coq.ZArith.ZArith Coq.QArith.QArith Coq.Reals.Reals Coq.setoid_ring.Field_tac Coq.setoid_ring.Ring_tac Coq.fourier.Fourier.

Coercion inject_Z : Z >-> Q.

Ltac begin := unfold inject_Z; simpl; intros.

Ltac arith := solve [ nsatz | omega | lia | nia | nra | lra | fourier | field | ring ].

Goal True.

  Fail assert (forall k, (2 < k -> 2^k * 2^(k-2) = 4^(k-1))%Q%Z) by (begin; arith).

  Fail assert (forall k, (2 < k -> 2^k * 2^(k-2) = 4^(k-1))%Z) by (begin; arith).

  Fail assert (forall k, (2 < k -> 2^k * 2^(k-2) = 4^(k-1))%R) by (begin; arith).

  (** This is provable with just lemmas in the standard library... *)

  assert (forall k, (2 < k -> 2^k * 2^(k-2) = 4^(k-1))%Z).

  { intros.

    assert (H0 : (4 = 2^2)%Z) by lia.

    assert (H1 : (2^k * 2^(k-2) = 2^(k + (k - 2)))%Z) by (rewrite Z.pow_add_r; lia).

    assert (H2 : (k + (k - 2) = 2 * k - 2)%Z) by lia.

    assert (H3 : ((2^2)^(k-1) = 2^(2*(k-1)))%Z) by (rewrite Z.pow_mul_r; lia).

    assert (H4 : (2*(k-1) = 2 * k - 2)%Z) by lia.

    congruence. }

Thanks,

Jason