Stream: Coq users

Topic: An eqP lemma


view this post on Zulip Julin Shaji (Mar 31 2024 at 12:32):

I got a type like

Require Import ssreflect.
Require Import Bool.

Inductive t: Type :=
| Zero: t
| One: t
| More: t -> t -> t.

And have made a equality procedure for it:

Fixpoint teqb (a b: t): bool :=
  match a, b with
  | Zero, Zero => true
  | One, One => true
  | More a1 b1, More a2 b2 => teqb a1 a2 && teqb b1 b2
  | _, _ => false
  end.

Now, I am trying to have an eqP reflection lemma:

Lemma eqtP (a b: t): reflect (a = b) (teqb a b).
Proof.
    elim: a b => [b|b|a IHa b IHb].
    - case: b.
        + by apply ReflectT.
        + by apply ReflectF.
        + move => a b.
          by apply ReflectF.
    - case: b.
        + by apply ReflectF.
        + by apply ReflectT.
        + by move => a b; apply ReflectF.
  - case.
      + by apply ReflectF.
      + by apply ReflectF.
      + move => x y.
(*
1 subgoal

a : t
IHa : forall b : t, reflect (a = b) (teqb a b)
b : t
IHb : forall b0 : t, reflect (b = b0) (teqb b b0)
x, y : t

========================= (1 / 1)

reflect (More a b = More x y) (teqb (More a b) (More x y))
*)

And am stuck at the induction step.

Any idea how I can proceed from here?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2024 at 12:56):

@Julin Shaji , indeed there are several ways to do this kind of proof, I usually split the proof in several sublemmas, but that's not necessary in this case, as it is pretty simple and you can handle a direct proof:

From mathcomp Require Import all_ssreflect.

Inductive t: Type :=
| Zero: t
| One: t
| More: t -> t -> t.

Fixpoint teqb (a b: t): bool :=
  match a, b with
  | Zero, Zero => true
  | One, One => true
  | More a1 b1, More a2 b2 => teqb a1 a2 && teqb b1 b2
  | _, _ => false
  end.

Lemma teqbb a : a = a -> teqb a a.
Proof. by elim: a => //= ? ht1 ? ht2 _; rewrite ht1 ?ht2. Qed.

Lemma teqb_refl a b : a = b -> teqb a b.
Proof. by elim: a b => [||? ? ? ?] [||] // a2 b2 [->->]; rewrite !teqbb. Qed.

Lemma teqb_correct a b : teqb a b -> a = b.
Proof.
by elim: a b => [||t1 ih1 t2 ih2] [||t1' t2'] //= /andP[/ih1->/ih2->].
Qed.

Lemma eqtP (a b: t): reflect (a = b) (teqb a b).
Proof.
by apply: (iffP idP); [apply: teqb_correct|apply: teqb_refl].
Qed.

Lemma eqtP_direct a b : reflect (a = b) (teqb a b).
Proof.
elim: a b => [||a1 iha b1 ihb] [||] //=; try constructor; move=> // t1 t2.
by have [->|hnea]:= iha t1; have [->|hneb] := ihb t2; constructor; try case.
Qed.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2024 at 12:57):

It is often convenient to show that a type has some property by just showing and embedding into some type that already has the structure, tho that will result in an equality that doesn't compute as is.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2024 at 12:58):

The point you are stuck in the proof is because it is time to use the induction hyp; you need to check what the equality on subterms resulted before you can decide what the right result is.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2024 at 13:03):

You can do that a bit more step-by-step as:

      + move => x y /=.
        have [->|neqa] := IHa x; last by constructor; case.
        by have [->|neqb] := IHb y; constructor; try case.

view this post on Zulip Quentin VERMANDE (Mar 31 2024 at 13:43):

You can also use iffP idP to turn a goalreflect P b into two implications P -> b and b -> P (you can even apply the reflection you want to b instead of idP).


Last updated: Jun 13 2024 at 19:02 UTC