The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Thanks, Jason.

I realized, from your clue about getting everything to recurse over lb,
that I could simplify the problem by using a predicate that more
closely mirrors the definition of truebits by recursing it over lb:

Fixpoint ok_truebits(i:nat)(ln:list nat)(lb:list bool) : Prop :=
  match lb with
  | true :: lb => In i ln /\ ok_truebits (S i) ln lb
  | false :: lb => ok_truebits (S i) ln lb
  | nil => True
  end.

This, plus a few more simple lemmas, made it easy to prove
forall lb i, ok_truebits i (truebits i lb) lb.  No offsets needed.

On Wed, 22 Jul 2020 23:37:49 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> 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?*)
> >
> >