coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] obligations
Date: Mon, 9 May 2016 16:32:26 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
Ironport-phdr: 9a23:VfQmAR1uNK4JKeIesmDT+DRfVm0co7zxezQtwd8ZsegVK/ad9pjvdHbS+e9qxAeQG96LurQd0KGM6ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZ3snLrrs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDWG6noZGlcflhtWCkCR8gPzWpbvuwPxs/c71SWHa56lBYsoUCivuv84ACTjjz0KYmY0

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.

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] obligations, Vadim Zaliva, 05/10/2016
- Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
- Re: [Coq-Club] obligations, Daniel Schepler, 05/10/2016
  - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
    - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
      - Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/11/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/12/2016
        
        Re: [Coq-Club] obligations, Matthieu Sozeau, 05/12/2016