Strengthening inductive hypothesis for lists?

Using Coq
1

Hello,

I have an inductive type that uses list. When trying to prove things by induction on on it, I can’t manage to get an induction hypothesis for the elements of the list:

Inductive things : Type :=
| B : bool -> things
| A : list things -> things.

Inductive is_true : things -> Prop :=
| Foo_B : forall b, b = true -> is_true (B b)
| Foo_A : forall ts, Forall is_true ts -> is_true (A ts).

Fixpoint is_trueb (t : things) : bool :=
  match t with
  | B b => b
  | A ts => forallb is_trueb ts
  end.

Lemma sound: ∀ t,
    is_trueb t = true -> is_true t.
Proof.
  induction t.
  - (* B *) simpl. constructor. assumption.
  - (* A *) (* I'm here *)

At this point I have to prove:

  l : list things
  ============================
  is_trueb (A l) = true → is_true (A l)

and I would ideally like to have a hypothesis of the form:

H : forall x, In x l -> is_trueb x = true -> is_true x

Any ideas how to go about this? Thanks!

2

You may have a look at Nested Inductive Types.

1 Like