Stream: Coq users

Topic: ✔ A proof with dependent types


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julin Shaji (Mar 04 2024 at 11:26):

Oh.. right. :+1:

view this post on Zulip Julin Shaji (Mar 04 2024 at 11:27):

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.

view this post on Zulip Notification Bot (Mar 04 2024 at 11:38):

Julin Shaji has marked this topic as resolved.

view this post on Zulip 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