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: Oct 13 2024 at 01:02 UTC