## Stream: Coq users

### Topic: ✔ A proof with dependent types

#### Julin Shaji (Mar 04 2024 at 11:07):

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

#### Johannes Hostert (Mar 04 2024 at 11:12):

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.

#### Julin Shaji (Mar 04 2024 at 11:18):

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

#### Johannes Hostert (Mar 04 2024 at 11:24):

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:

#### Julin Shaji (Mar 04 2024 at 11:27):

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

#### Notification Bot (Mar 04 2024 at 11:38):

Julin Shaji has marked this topic as resolved.

#### Notification Bot (Mar 04 2024 at 15:00):

Julin Shaji has marked this topic as resolved.

Last updated: Jun 22 2024 at 16:02 UTC