The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You need to generalize your theorem statement to be about truebits, maybe something like

Fixpoint are_truebits_gen (offset : nat) (ln:list nat)(lb:list bool) : Prop :=

  match ln with

  | i :: ln => nth_error (i - offset) lb = Some true /\ are_truebits_gen offset ln lb

  | nil     => True

  end.

Theorem all_truebits_are_truebits_gen: 

  forall lb offset, are_truebits_gen offset (truebits offset lb) lb.

Now you should just be able to induct over lb (while still universally quantified over offset), and everything is structurally recursive over lb, so you can just simplify.  Then you do a bit of arithmetic to apply your inductive hypothesis.

The general rule of thumb is that if your inductive hypothesis doesn't apply because some constant doesn't line up, you need to generalize your theorem statement to one that holds for all values of that constant.

On Wed, Jul 22, 2020, 23:30 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I know there is a trick to this kind of proof, and I may have seen it a
few times, but I don't remember it.  I would appreciate anyone's help
with this:

From Coq Require Import Lists.List.
Import ListNotations.

Fixpoint truebits(i:nat)(lb:list bool) : list nat :=
  match lb with
  | true  :: lb  => i :: truebits (S i) lb
  | false :: lb  =>      truebits (S i) lb
  | nil          => nil
  end.

(*list of indexes of true in lb*)
Definition all_truebits lb := truebits 0 lb.

(*if all indexes in ln are indexes of true in lb*)
Fixpoint are_truebits(ln:list nat)(lb:list bool) : Prop :=
  match ln with
  | i :: ln => (nth i lb false) = true /\ are_truebits ln lb
  | nil     => True
  end.

Theorem all_truebits_are_truebits:
  forall lb, are_truebits (all_truebits lb) lb.
(*How to prove this?*)