The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  Maybe you need to do a bit of intros/subst before calling ring?

-- Matthieu

On Tue, May 10, 2016 at 1:32 AM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

I am having some trivial problems with solving obligations under 8.5. It goes like this:

  Obligation Tactic := ring.

  Show Obligation Tactic. (* shows ring *)

  Solve All Obligations with ring.

  Show Obligation Tactic. (* still shows ring *)

  Program Definition Eq23 (m0 n0 v:nat)

    := (* omitted *).

Eq23 has type-checked, generating 4 obligation(s)

Solving obligations automatically...

4 obligations remaining

Obligation 1 of Eq23:

(∀ (m0 n0 v : nat) (m:=(m0 * v)%nat) (n:=(n0 * v)%nat),

 (m * n)%nat = (m * n0 * v)%nat).

Obligation 2 of Eq23:

(∀ (m0 n0 v : nat) (m:=(m0 * v)%nat) (n:=(n0 * v)%nat),

 (n * v)%nat = (n0 * (v * v))%nat).

Obligation 3 of Eq23:

(∀ (m0 n0 v : nat) (m:=(m0 * v)%nat) (n:=(n0 * v)%nat),

 (m0 * (n0 * (v * v)))%nat = (m * n)%nat).

Obligation 4 of Eq23:

(∀ (m0 n0 v : nat) (m:=(m0 * v)%nat) (n:=(n0 * v)%nat),

 (m0 * n0 * v * v)%nat = (m0 * (n * v))%nat).

At this point I have to solve them manually.

  Next Obligation. Proof. ring. Qed.

  Next Obligation. Proof. ring. Qed.

  Next Obligation. Proof. ring. Qed.

  Next Obligation. Proof. ring. Qed.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060