Stream: Coq users

Topic: Proving equality of a dependent type


view this post on Zulip Julin Shaji (Mar 06 2024 at 04:51):

I have a type like this:

Inductive t: nat -> bool -> Type :=
| Nil: t 0 false
| Pad: forall {n: nat} {b: bool},
    t n b -> t (S n) b
| Mark: forall {n: nat},
    t n false -> t (S n) true.

Now I wanted to write a function saying whether any two given values of
t n are equal or not.

So I started writing a function like this:

Fixpoint eqb {b1 b2: bool}: forall n:nat, t n b1 -> t n b2 -> bool.
refine (fun n o1 o2 => _).
  refine (
    match o1, o2 with
    | Nil, Nil => true
    | Pad n1' b1' o1', Pad n2' b2' o2' => _
    | Mark n1' o1', Mark n2' o2' => _
    | _, _ => false
    end).
(*
2 subgoals

eqb : forall (b1 b2 : bool) (n : nat), t n b1 -> t n b2 -> bool
b1, b2 : bool
n : nat
o1 : t n b1
o2 : t n b2
n1' : nat
b1' : bool
o1' : t n1' b1'
n2' : nat
b2' : bool
o2' : t n2' b2'

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

bool

========================= (2 / 2)

bool
*)

But I can't make coq remember that n1' and n2' will be the same.

How can this be dealt with?

view this post on Zulip Julin Shaji (Mar 06 2024 at 04:53):

I've got this loaded From mathcomp Require Import all_ssreflect..

For some reason that seems to allow us to write the implicit arguments of the constructors as if they were explicit during the pattern matching.

view this post on Zulip Julin Shaji (Mar 06 2024 at 05:10):

I think I could prove a more general theorem though:

Fixpoint eqb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
  case (Nat.eqb n1 n2) eqn:Hneq.
  move/PeanoNat.Nat.eqb_spec: Hneq => Hneq.
  refine (
    match o1, o2 with
    | Nil, Nil => true
    | Pad n1' b1' o1', Pad n2' b2' o2' => _
    | Mark n1' o1', Mark n2' o2' => _
    | _, _ => false
    end).
  - move: n1' n2' o1' o2' => n1' n2'.
    case (Nat.eqb n1' n2') eqn:Hneq'.
    + move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'.
      rewrite -Hneq'.
      move => o1' o2'.
      exact: eqb _ _ _ _ o1' o2'.
    + exact: (fun _ _ => false).
  - move: n1' n2' o1' o2' => n1' n2'.
    case (Nat.eqb n1' n2') eqn:Hneq'.
    + move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'.
      rewrite -Hneq'.
      move => o1' o2'.
      exact: eqb _ _ _ _ o1' o2'.
    + exact: (fun _ _ => false).
  - exact: false.
Defined.

view this post on Zulip Julin Shaji (Mar 06 2024 at 05:21):

Would it be possible to do this without reflection?

view this post on Zulip Julin Shaji (Mar 06 2024 at 05:41):

I guess this is another way:

Fixpoint eqb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
  case (Nat.eqb n1 n2) eqn:Hneq.
  have Hn := iffLR (PeanoNat.Nat.eqb_eq n1 n2) Hneq.
  clear Hneq; rename Hn into Hneq.
  - refine (
      match o1, o2 with
      | Nil, Nil => true
      | Pad n1' b1' o1', Pad n2' b2' o2' => _
      | Mark n1' o1', Mark n2' o2' => _
      | _, _ => false
      end).
    + case (Nat.eqb n1' n2') eqn:Hneq'.
      * have Hn := iffLR (PeanoNat.Nat.eqb_eq n1' n2') Hneq'.
        clear Hneq'; rename Hn into Hneq'.
        rewrite -Hneq' in o2'.
        exact: eqb _ _ _ _ o1' o2'.
      * exact: false.
    + case (Nat.eqb n1' n2') eqn:Hneq'.
      * have Hn := iffLR (PeanoNat.Nat.eqb_eq n1' n2') Hneq'.
        clear Hneq'; rename Hn into Hneq'.
        rewrite -Hneq' in o2'.
        exact: eqb _ _ _ _ o1' o2'.
      * exact: false.
  - exact: false.
Defined.

view this post on Zulip Pierre Roux (Mar 06 2024 at 07:59):

It may be an XY problem. If I were you, I probably wouldn't use your type t in the first place and just resort to lists of Pad | Mark, paired with proofs about their size / non emptiness. That will likely be much easier to handle. Just like tuples are most of the time much more convenient than vectors.

view this post on Zulip Dominique Larchey-Wendling (Mar 06 2024 at 12:41):

It is often the case that you can write a decider for eq on an inductive type, say {x=y}+{x≠y} by induction on x and then dependent inversion on y. So what you need is inversion lemmas for your type.

view this post on Zulip Ali Caglayan (Mar 06 2024 at 15:09):

Here is a way to do what you want:

Definition eqb {n m} {b b'} : t n b -> t m b' -> bool.
Proof.
  intros x.
  induction x as [|? ? ? eqb_x|? ? eqb_x] in m, b' |- *.
  - intros y.
    destruct y.
    1: exact true.
    1,2: exact false.
  - intros y.
    destruct y as [|? ? y'|].
    1,3: exact false.
    exact (eqb_x _ _ y').
  - intros y.
    destruct y.
    1,2: exact false.
    exact (eqb_x _ _ y).
Defined.


Eval cbv in (eqb Nil Nil).
Eval cbv in (eqb Nil (Pad Nil)).
Eval cbv in (eqb (Pad Nil) (Pad Nil)).
Eval cbv in (eqb (Pad Nil) Nil).
Eval cbv in (eqb (Mark Nil) (Mark Nil)).
Eval cbv in (eqb (Mark Nil) (Mark (Pad Nil))).

I haven't actually proven that it reflects to equality, but that is something you can try. I just added some tests to convince myself that it is correct.

view this post on Zulip Ali Caglayan (Mar 06 2024 at 15:10):

You can use fixpoint, but it quickly gets tricky since you have to make sure you have a decreasing argument. Instead, you can use the induction tactic in proof mode which let's you use the dependent eliminator of t without having to think about the fixpoint.

view this post on Zulip Ali Caglayan (Mar 06 2024 at 15:11):

Basically I define a generic eqb, and by induction I can just compare the arguments of the constructors.

view this post on Zulip Ali Caglayan (Mar 06 2024 at 15:13):

Also I concur with Pierre that the type t isn't great. Indexed inductive types (other than equality) are not really easy to work with. It's generally better to pick a non-indexed type and then perhaps define an inductive predicate on that which carves out the valid terms you want.

view this post on Zulip Dominique Larchey-Wendling (Mar 06 2024 at 23:21):

Here is a solution using dependent inversion. Doing the exercise I realize that I forgot to pinpoint one tricky aspect which is the injectivity of constructors on dependent inductive types.

Inductive t: nat -> bool -> Type :=
| Nil: t 0 false
| Pad: forall {n: nat} {b: bool},
    t n b -> t (S n) b
| Mark: forall {n: nat},
    t n false -> t (S n) true.

(* A statement for the inversion lemma on t *)
Definition t_inv_type n b : t n b -> Type :=
  match n with
  | 0 => match b with
    | true  => fun _ => False
    | false => fun x => Nil = x
    end
  | S m => fun x => ({ x' | Pad x' = x } +
      match b return t _ b -> _ with
      | false => fun _ => False
      | true  => fun x => { x' : t _ false | Mark x' = x }
      end x)%type
  end.

(* The proof is easy *)
Fact t_inv {n b} x : t_inv_type n b x.
Proof.
  destruct x as [ | n b x | n x ]; simpl.
  + trivial.
  + left; now exists x.
  + right; now exists x.
Qed.

(** Now proofs that the constructors of t are injective.
    These are a bit tricky because one needs dependent projections
    like those which can be found in the Braga method.

    An alternative is using decidable equality of the dependent
    parameters (see Eqdep_dec). *)

Definition is_Pad {n b} (x : t n b) :=
  match x with
  | Pad _ => True
  | _ => False
  end.

Definition is_Mark {n b} (x : t n b) :=
  match x with
  | Mark _ => True
  | _ => False
  end.

Definition t_proj2 {n b} (x : t n b) : is_Pad x -> t (pred n) b :=
  match x with
  | Nil => fun C => match C with end
  | Pad x => fun _ => x
  | Mark x => fun C => match C with end
  end.

Definition t_proj3 {n b} (x : t n b) : is_Mark x -> t (pred n) false :=
  match x with
  | Nil => fun C     => match C with end
  | Pad x => fun C   => match C with end
  | Mark x => fun _  => x
  end.

Fact t_proj2_feq n b (x y : t n b) Hx Hy : x = y -> t_proj2 x Hx = t_proj2 y Hy.
Proof.
  intros <-; f_equal; destruct x; simpl in *.
  1,3: easy.
  now destruct Hx; destruct Hy.
Qed.

Fact t_proj3_feq n b (x y : t n b) Hx Hy : x = y -> t_proj3 x Hx = t_proj3 y Hy.
Proof.
  intros <-; f_equal; destruct x; simpl in *.
  1,2: easy.
  now destruct Hx; destruct Hy.
Qed.

Lemma Pad_inj n b (x y : t n b) : Pad x = Pad y -> x = y.
Proof.
  intros H.
  change (t_proj2 (Pad x) I = t_proj2 (Pad y) I).
  revert H; apply t_proj2_feq.
Qed.

Lemma Mark_inj n (x y : t n false) : Mark x = Mark y -> x = y.
Proof.
  intros H.
  change (t_proj3 (Mark x) I = t_proj3 (Mark y) I).
  revert H; apply t_proj3_feq.
Qed.

(* Now the decider for equality is easy by induction on
   x and dependent inversion on y *)
Theorem t_eqdec n b (x y : t n b) : { x = y } + { x <> y }.
Proof.
  induction x as [ | | ] in y |- *; generalize (t_inv y); simpl.
  + now left.
  + intros [ (y' & <-) | H ].
    * destruct (IHx y') as [ <- | D ].
      - now left.
      - right; contradict D.
        now apply Pad_inj.
    * destruct b.
      - destruct H as (? & <-); now right.
      - easy.
  + intros [ (y' & <-) | (y' & <-) ].
    * now right.
    * destruct (IHx y') as [ <- | D ].
      - now left.
      - right; contradict D.
        now apply Mark_inj.
Qed.

view this post on Zulip Dominique Larchey-Wendling (Mar 07 2024 at 14:34):

And with a fixpoint:

Fixpoint t_eq_dec {n b} (x : t n b) { struct x } : y, { x = y } + { x  y }.
Proof.
  refine (match x with
  | Nil         => λ y,
    match t_inv y with
    | t_inv_t1_1 => left _
    end
  | @Pad n b x  =>
    match b return  (x : t _ b) y, { Pad x = y } + { Pad x  y } with
    | true  => λ x y,
      match t_inv y with
      | t_inv_t3_1 _ y =>
        match t_eq_dec _ _ x y with
        | left e  => left _
        | right d => right _
        end
      | t_inv_t3_2 _ y => right _
      end
    | false => λ x y,
      match t_inv y with
      | t_inv_t2_1 _ y =>
        match t_eq_dec _ _ x y with
        | left  e => left _
        | right d => right _
        end
      end
    end x
  | @Mark n x   => λ y,
    match t_inv y with
    | t_inv_t3_1 _ y => right _
    | t_inv_t3_2 _ y =>
      match t_eq_dec _ _ x y with
      | left  e => left _
      | right d => right _
      end
    end
  end); easy || subst; auto.
Defined.

view this post on Zulip Julin Shaji (Mar 15 2024 at 16:32):

Pierre Roux said:

I probably wouldn't use your type t in the first place and just resort
to lists of Pad | Mark, paired with proofs about their size / non
emptiness.

Yeah, that's what I probably would've been better of doing.
I often find myself wandering towards indexed types though I've been
told multiple times that doesn't scale well.

Just like tuples are most of the time much more convenient than
vectors.

Had heard of this too. But didn't really get around to seeing how it's
done.
I guess there's an implementation like this in https://github.com/coq-community/bits/


Last updated: Jun 18 2024 at 22:01 UTC