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?

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.

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.
```

Would it be possible to do this without reflection?

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.
```

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.

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.

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.

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.

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

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.

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.
```

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.
```

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