CODEWITHSUNDEEP
coq
rpf
rpf

Reputation: 123

Coq: Insufficient Justification error

I am new to Coq and am getting an Insufficient Justification error for hypothesis H3. I tried rewriting it several times but the error persists. Could someone please explain why? Thanks.

Section GroupTheory.
Variable G: Set.
Variable operation: G -> G -> G.
Variable e : G.
Variable inv : G -> G.
Infix "*" := operation.

Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z).
Hypothesis identity : forall x : G, exists e : G, (x * e = x) /\ (e * x = x).
Hypothesis inverse : forall x : G, (x * inv x = e) /\ (inv x * x = e).

Theorem latin_square_property : 
  forall a b : G, exists x : G, a * x = b.
proof.
  let a : G, b : G.
  take (inv a * b).
  have H1:(a * (inv a * b) = (a * inv a) * b) by associativity.
  have H2:(a * inv a = e) by inverse.
  have H3:(e * b = b) by identity.
  have (a * (inv a * b) = (a * inv a) * b) by H1.
                       ~= (e * b) by H2.
                       ~= (b) by H3.
hence thesis.
end proof.
Qed.
End GroupTheory.

Upvotes: 2

Views: 61

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

The reason is that your identity axiom is independent of the unit e, defined in the section, because you've bound e with the existential quantifier in the definition of the identity axiom.

We can amend identity, getting rid of exists e in the definition:

Hypothesis identity : forall x : G, (x * e = x) /\ (e * x = x).

After that you'll be able to finish your proof.

Upvotes: 2

Related Questions