I have a dependent type like:

```
Require Import ssreflect.
Inductive taux: nat -> bool -> Type :=
| Nil: taux 0 false
| Pad: forall {n: nat} {b: bool},
taux n b -> taux (S n) b
| Mark: forall {n: nat},
taux n false -> taux (S n) true.
Fixpoint markCount_aux {n: nat} {b: bool} (a: taux n b): nat :=
match a with
| Nil => 0
| Pad a' => markCount_aux a'
| Mark a' => S (markCount_aux a')
end.
Definition markCount {n: nat} (a: taux n true): nat :=
markCount_aux a.
```

Then I was trying to prove this:

```
Goal forall (n: nat) (a: taux n true),
markCount a = 1.
Proof.
move => n a.
elim: n a => [a|n IH a]; first by inversion a.
(*
1 subgoal
n : nat
IH : forall a : taux n true, markCount a = 1
a : taux (S n) true
========================= (1 / 1)
markCount a = 1
*)
```

But am stuck here.

Is there a way to get to deal with the individual constructors of `taux`

?

State the induction hypothesis for the `_aux`

variant, so that you can state it with unconstrainted indices, so that regular induction on `a : taux n b`

works. It would likely be something like `markCont_aux a = if b then 1 else 0`

.

Then your lemma is just a special case of the more general one.

Thanks!

I guess it would be something like this:

```
Lemma foo: forall (n: nat) (b: bool) (a: taux n b),
markCount_aux a = if b then 1 else 0.
Proof.
move => n b a.
elim/taux_ind: a => //=.
by move => n' a' ->.
Qed.
```

I don't think the `taux_ind`

is necessary, `elim`

selects it automatically as it is the regular normal standard induction principle on `taux`

Oh.. right. :+1:

Made it like:

```
Lemma lmCountMark: forall (n: nat) (b: bool) (a: taux n b),
markCount_aux a = if b then 1 else 0.
Proof.
move => n b a.
elim: a => //=.
by move => n' a' ->.
Qed.
Lemma lmCountMarkTrue: forall (n: nat) (a: taux n true),
markCount a = 1.
Proof.
move => n a.
exact: (lmCountMark n true a).
Qed.
```

Julin Shaji has marked this topic as resolved.

Julin Shaji has marked this topic as resolved.

Last updated: Jun 22 2024 at 16:02 UTC