How to state mutual/nested lemmas

Using Coq
1

Hi ! I have a nested inductive type that look like a tree, with a custom induction principle to account for the nested usage of list: shack/lang.v at main · facebookresearch/shack · GitHub

So far I never had to state mutually recursive properties on both lang_ty and list lang_ty, so this induction principle was enough.

I am now facing a situation where I want to mutually prove something on them. Something like (∀ ty : lang_ty, P ty) /\ (∀ tys: list lang_ty, Q tys). With a mutual inductive family, I could use Lemma .. with to state this, but I don’t know how to do this for a nested inductive (or if that’s even possible).

Should I go back and change to a mutual inductive in the first place, or is there a way to state a mutual lemma when using nested inductive types ?

2

How do you expect to prove ∀ tys: list lang_ty, Q tys? If you can prove ∀ tys: list lang_ty, Forall P tys -> Q tys, then the following might suit you:

Variable P : lang_ty -> Prop.
Variable Q : list lang_ty -> Prop.
...
Hypothesis case_ClassT : forall cname targs, Q targs -> P (ClassT cname targs).
Hypothesis case_List : forall targs, Forall P targs -> Q targs.
...

Definition _lang_ty_list_ind (lang_ty_ind : forall t : lang_ty, P t) (l : list lang_ty)  : Q l :=
    let H := (fix fold (xs : list lang_ty) : Forall P xs :=
          match xs with
          | nil => List.Forall_nil _
          | x :: xs => List.Forall_cons x (lang_ty_ind x) (fold xs)
          end) l in
        case_List _ H.

  Fixpoint lang_ty_ind (t : lang_ty) : P t :=
    match t with
    ...
    | ClassT cname targs => case_ClassT cname targs (_lang_ty_list_ind lang_ty_ind targs)
    ...
    end.

  Definition lang_ty_list_ind : forall tys : list_lang_ty, Q tys := _lang_ty_list_ind (lang_ty_ind).

I’ll admit it’s probably not the nicest presentation, but it works.
This is the kind of induction principle we use for typing in MetaCoq (with a specific case going from a Forall over a list to the predicate we’re interested in), and it seems to work quite well there. The main difference is that we do not prove the induction principle directly by induction on the structure, but via an auxiliary definition of size.

2 Likes
3

I faced a similar problem but worse with nested inductive coinductive types.

IIRC it was Brouwer ordinals that are defined as

Inductive ord := O | S (n: ord) | Lim (p: nat -> ord).

In a futile attempt to avoid extensionality I wanted to try

CoInductive stream A := cons {
  head: A ;
  tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Lim (p: stream ord).

But no turns out induction over this encoding is impossible even using sized types in Agda

Anyhow I’d suggest if possible you’d use an encoding like

| ClassT (cname: tag) (n: nat) (targs: Fin.t n -> lang_ty)

That way you don’t need a custom induction principle.

You can also try converting back and forth between this funky encoding and lists or vectors but IDK how well that’d work.

4

That’s an interesting idea! But it’ll probably require extensionality to define decidable equality, and migration is probably going to be annoying.

5

Thank you for these suggestions, they are very interesting !
FYI I managed to get around this mutual induction by splitting the problem into smaller bits, that were no longer mutual.

Still I found all this feedback very valuable, thank you

6

I don’t think extensionality is a problem when you have a function out of the finites. But yeah might not be the nicest encoding.

7

You can use Fixpoint <lemma_name> <params> {struct <param>} : <statement>. Proof. ... Qed. and even Fixpoint ... with ... Proof. ... Qed.

1 Like
8

My understanding is that Fixpoint…with is like Lemma…with and will only work with mutual inductive definitions, not nested ones. Am I missing something ?

9

For a nested, non-mutual inductive type, a single Fixpoint lemma can do the trick:

Section nested_ind.

  Inductive tree :=
  | Leaf : nat -> tree
  | Single : tree -> tree
  | Node : list tree -> tree.

  Variable P : tree -> Prop.
  Variable Q : list tree -> Prop.

  Variable LeafCase : forall n, P (Leaf n).
  Variable SingleCase : forall t, P t -> P (Single t).
  Variable NodeCase : forall l, Q l -> P (Node l).
  Variable NilCase : Q nil.
  Variable ConsCase : forall t l, P t -> Q l -> Q (cons t l).

  Definition ind_list (l : list tree) (IHt : forall t, P t) : Q l.
  Proof.
    induction l.
    - apply NilCase.
    - apply ConsCase.
       + apply IHt.
       + apply IHl.
  Defined.

  Fixpoint ind (t : tree) {struct t} : P t.
  Proof.
    destruct t.
    - apply LeafCase.
    - apply SingleCase.
      apply ind.
    - apply NodeCase.
      apply ind_list.
      apply ind.
  Qed.

End nested_ind.