1
$\begingroup$

I'm trying to represent Boole-Schroder Algebra in Coq, and am trying to use apply to start a proof using one of my defined axioms, but I'm getting an "unable to unify" error. Why can't I use apply with that axiom?

Class BooleSchroderAlgebra (A : Type) := {
  zero : A;  (* null class *)
  one : A;  (* universe of discourse class *)
  union : A -> A -> A;
  inter : A -> A -> A;
  neg : A -> A;
  contains : A -> A -> Prop;
  
  neg_zero : neg zero = one;
  neg_one : neg one = zero;
  union_def : forall a b, union a b = neg(inter (neg a) (neg b));
  contains_def : forall a b, contains a b -> inter a b = a;
  
  identity : forall a, inter a a = a;
  inter_comm : forall a b, inter a b = inter b a;
  inter_assoc : forall a b c, inter a (inter b c) = inter (inter a b) c;
  inter_zero : forall a, inter a zero = zero;
}.

Theorem inter_neg_zero_contains : forall (A : Type) (BSA : BooleSchroderAlgebra A) (a b : A),
  inter a (neg b) = zero -> contains a b.
Proof.
  intros A BSA a b H.
  apply contains_def.

The error I'm getting:

A : Type
BSA : BooleSchroderAlgebra A
a, b : A
H : inter a (neg b) = zero
Unable to unify "inter ?M826 ?M827 = ?M826" with
 "(let
  (zero, one, union, inter, neg, contains, _, _, _, _, _, _, _,
 _) :=
  BSA in
contains)
  a
  b".
Improve this question
$\endgroup$
2
  • $\begingroup$ Aren't you missing some axioms about how intersection and negation interact? And also, how negation interacts with itself (ie, being involutive)? Without this, I don't think you will be able to prove your goal. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Jun 19 at 8:36
  • $\begingroup$ It would be more convenient to axiomatize such algebras without union and deifne unions by Definition union a b := neg (inter (neg a) (neg b)). $\endgroup$
    – Andrej Bauer
    Commented Jun 19 at 16:08

1 Answer 1

Reset to default
1
$\begingroup$

I think you are reading your implication in the wrong order. It seems to me you are trying to prove A => B knowing B => A

Improve this answer
$\endgroup$
4
  • $\begingroup$ At that point in the proof, the goal is contains a b. contains_def maps from that to a different proposition which is possible to work with. I should expect to be able to change the proof goal to that different proposition by applying the implication. $\endgroup$
    – Lisanna Dettwyler
    Commented Jun 18 at 19:31
  • $\begingroup$ In that case you probably want contains_def : forall a b, contains a b <-> inter a b = a; $\endgroup$
    – djao
    Commented Jun 18 at 20:00
  • $\begingroup$ In general if your goal is Q then you can apply an implication of the form P -> Q to change your goal to P. You can't apply an implication of the form Q -> R on a goal of Q. That's how implication works. Logic is a one-way street unless you have double-sided arrows. $\endgroup$
    – djao
    Commented Jun 18 at 20:07
  • $\begingroup$ @LisannaDettwyler from your response it is clear that you are trying to use your axiom the wrong way. If you yuo know cow : A → B and you are trying to prove B, then apply cow will change the goal to A. This is so from A → B and A it follows that B. $\endgroup$
    – Andrej Bauer
    Commented Jun 19 at 16:07

Not the answer you're looking for? Browse other questions tagged or ask your own question.