1

Trying to prove MT1A with MT1 (or MT1bis), but Coq fails to unify:

Require Export Classical_Prop.
Require Export Classical_Pred_Type.

Variable MT : Type.
Parameter NIL : MT.
Variables a b e : MT -> MT.
Variable c : MT * MT -> MT.

Axiom MT1 :
  forall x y z: MT, z = c(x,y) -> a(z) = x /\ b(z) = y.

Axiom MT1bis :
  forall x y z: MT, z = c(x,y) <-> a(z) = x /\ b(z) = y.

Axiom MT3 :
  forall x y z : MT, z = c(a(z),b(z)) <-> a(z) <> z /\ b(z) <> z.

Definition example := c(NIL, e NIL).

Lemma MT1A :
  forall x: MT, x = a (c(example, b example)) -> x = example /\ a x <> x /\ b x <> x.
Proof.
(*  unfold example. *)
  intros.
  apply MT1. (* ??? *)

Qed.

Which tactics can be used here to hint Coq how to get c() out of a()? (One possibility also is, that those axioms are not enough for the proof, though at first glance they are. If MT1 is not enough, maybe MT1bis is?)

Tried to find suitable tactics, like rewrite, but it did not work (maybe, needed more complex hint). Can't find any more tactics, which can help.

(this is not homework assignment, just one hobby project)

Roman Susi
  • 4,135
  • 2
  • 32
  • 47

1 Answers1

2

I removed unused variables from MT3:

Axiom MT3 :
  forall z : MT, z = c(a(z),b(z)) <-> a(z) <> z /\ b(z) <> z.

We can use the remember tactic to kind of "extract" a term from inside a larger term (and remember this connection in an equation):

Lemma MT1A x :
  x = a (c (example, b example)) ->
  x = example /\ a x <> x /\ b x <> x.
Proof.
  unfold example; intros H.
  rewrite <-MT3.
  remember (c (NIL, e NIL)) as f eqn:F.
  pose proof (MT1 _ _ _ F) as [F1 F2].
  remember (c (f, b f)) as g eqn:G.
  pose proof (MT1 _ _ _ G) as [G1 G2].
  split; congruence.
Qed.
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • 1
    Ok, thanks!. Three new tactics here for me... and correct use of rewrite (I've added `Require Import Coq.Setoids.Setoid.` for example to pass) – Roman Susi Jan 01 '18 at 16:05
  • I didn't add any imports except `Require Classical_Prop.` and it worked for me (I'm on Coq 8.7.1). – Anton Trunov Jan 01 '18 at 16:09
  • I have ancient version: 8.4pl4. – Roman Susi Jan 01 '18 at 16:16
  • These days one can use OPAM package manager to work with modern Coq versions. I tried to cover more in [this answer](https://stackoverflow.com/a/43957326/2747511), after the preparation steps you can type `opam install coq` into your terminal and get a working Coq system. – Anton Trunov Jan 01 '18 at 16:20
  • Can't find in the docs: why `(MT1 _ _ _ F)` ? What those holes correspond to? – Roman Susi Jan 01 '18 at 17:12
  • 1
    They stand for `x`, `y`, `z` respectively. `MT1` has type `forall x y z: MT, z = c(x,y) -> a(z) = x /\ b(z) = y` and `x`, `y`, `z` can be inferred from the next argument of type `z = c(x,y)`, hence the three `_`. Alternatively, you could have declared the first three arguments as implicit: `Arguments MT1 [x y z]` (put this after `MT1`) and then you'd be able to `pose proof (MT1 F) as [F1 F2].`. Another option is to `Set Implicit Arguments.` after the imports (this is a global setting for your file). – Anton Trunov Jan 01 '18 at 17:36