Add generation of enhanced induction schemes

[MarvinLira]

Issue

closes #159

Description of the Change

To state the additional induction hypotheses, for any type with at least one type variable T a1 ... an an inductive type ForT of the following type is declared.

Inductive ForT (Shape : Type) (Pos : Shape -> Type) (a1 ... an : Type) (P1 : a1 -> Prop) ... (Pn : an -> Prop)
    : T Shape Pos a1 ... an -> Prop
  := ...

Also for any 1<=i<=n an inductive type InT_i of the following type is declared.

Inductive InT_i (Shape : Type) (Pos : Shape -> Type) (a1 ... an : Type)
    : ai -> T Shape Pos a1 ... an -> Prop
  := ...

The meaning of those types is the same as for ForFree and InFree:

• ForT Shape Pos a1 ... an P1 ... Pn x states that Pi y holds for any y : ai, 1<=i<=n, that is somehow included in x
• InT_i Shape Pos a1 ... an y x states that y is somehow included in x

To formalize the connection between those types, the following lemma is also generated for the type T.

Lemma ForT_forall  (Shape : Type) (Pos : Shape -> Type) (a1 ... an : Type) :
  forall (P1 : a1 -> Prop) ... (Pn : an -> Prop) (x : T Shape Pos a1 ... an),
    ForT Shape Pos a1 ... an P1 ... Pn x
    <->
    (  (forall y : a1, InT_1 Shape Pos a1 ... an y x -> P1 y)
       /\
       ...
       /\
       (forall y : an, InT_n Shape Pos a1 ... an y x -> Pn y)
    ).

As an example consider the following definition of a list.

data MyList a = MyNil | MyCons (a, MyList a)

Inductive ForMyList (Shape : Type) (Pos : Shape -> Type) (a : Type) (P : a -> Prop)
    : MyList Shape Pos a -> Prop :=
  | ForMyList_nil : ForMyList Shape Pos a P (@myNil Shape Pos a)
  | ForMyList_cons : forall (fp : Free Shape Pos (Pair Shape Pos a (MyList Shape Pos a))),
      (* The property which has to hold for the constructor argument [fp] *)
      ForFree Shape Pos (Pair Shape Pos a (MyList Shape Pos a))
        (* The property which has to hold for any pair in the monadic value *)
        (ForPair Shape Pos a (MyList Shape Pos a)
           (* The property which has to hold for any element in the first position of the pair *)
           P
           (* The property which has to hold for any list in the second position of the pair *)
           (ForMyList Shape Pos a P)
        )
        (* Apply the [ForFree] property to the constructor argument *)
        fp ->
     ForMyList Shape Pos a P (@myCons Shape Pos a fp)

Inductive InMyList_1 (Shape : Type) (Pos : Shape -> Type) (a : Type)
    : a -> MyList Shape Pos a -> Prop :=
  | InMyList_1_cons_fp_1 : forall  (x   : a),
                                   (p  : Pair Shape Pos a (MyList Shape Pos a))
                                   (fp  : Free Shape Pos (Pair Shape Pos a (MyList Shape Pos a))),
      (* The element [x] is in the first position of the pair [p] *)
      InMyPair_1 Shape Pos a (MyList Shape Pos a) x p ->
      (* The Pair [p] is in the monadic value [fp] *)
      InFree Shape Pos (Pair Shape Pos a (MyList Shape Pos a)) p fp ->
      InMyList_1 Shape Pos a x (@myCons Shape Pos a fp)
  | InMyList_1_cons_fp_2 : forall  (x   : a),
                                   (l : MyList Shape Pos a)
                                   (p  : Pair Shape Pos a (MyList Shape Pos a))
                                   (fp  : Free Shape Pos (Pair Shape Pos a (MyList Shape Pos a))),
      (* The element [x] is in the list [l] *)
      InMyList_1 Shape Pos a x l ->
      (* The list [l] is in the second position of the pair [p] *)
      InMyPair_2 Shape Pos a (MyList Shape Pos a) l p ->
      (* The Pair [p] is in the monadic value [fp] *)
      InFree Shape Pos (Pair Shape Pos a (MyList Shape Pos a)) p fp ->
      InMyList_1 Shape Pos a x (@myCons Shape Pos a fp)

With those definitions induction schemes are generated and proven.

Fixpoint MyList_Ind (Shape : Type) (Pos : Shape -> Type) (a : Type)
  (P : MyList Shape Pos a -> Prop) ->

  (H_nil :
    (* This is the goal for the case that a list is empty *)
    P (@myNil Shape Pos a)) ->

  (H_cons : forall (fp : Free Shape Pos (Pair Shape Pos a (MyList Shape Pos a))),
    (* This [ForFree] property is the induction hypothesis for the case that a list is nonempty *)
    ForFree Shape Pos  (Pair Shape Pos a (MyList Shape Pos a))
      (ForPair Shape Pos a (MyList Shape Pos) NoProperty P) fp ->
    (* This is the goal for the case that a list is nonempty *)
    P (@myCons Shape Pos a fp)) ->

  forall (l : MyList Shape Pos a), P l.
Proof.
  ...
Qed.

Alternate Designs

The first design for the ForT- properties was to have such an property for every type variable of T.

Inductive ForT_i (Shape : Type) (Pos : Shape -> Type) (a1 ... an : Type) (P : ai -> Prop)
    : T Shape Pos a1 ... an -> Prop
  := ...

With this design there were multiple simple ForT_i_forall lemmas instead of one complex lemma. As those ForT_i properties may depend on each other, they have to be defined in a single induction sentence. This is however not accepted by Coq because the arguments (P : ai -> Prop) have different types for different i. Moving these args on the right side of the colon leads to violations of the strict positivity restriction for Coq types in the further usage.

Inductive ForT_i (Shape : Type) (Pos : Shape -> Type) (a1 ... an : Type)
    : forall (ai -> Prop), T Shape Pos a1 ... an -> Prop
  := ...

Possible Drawbacks

Verification Process

Additional Notes

[MarvinLira]

At the moment the following restrictions are made when generating properties and induction schemes:

• Mutual recursion is ignored in properties.
  • If we have mutual recursive types

    data Foo a = F (Bar a)
    data Bar a = B (Foo a)

    the ForFoo and InFoo properties will not make statements about the values of type a included in Bar, this applies symmetrically to ForBar and InBar.
    The same applies to mutual recursion with the same type but changed type variables.

    data Foo a b = F (Foo b a)

    The reason for this is that allowing this kind of recursion would make it necessary for the proofs of the forall lemmas to be fixpoint proofs and make them way harder than they are now, especially when using the auto tactic which tends to use the fixpoint hypothesis as early as possible and produce ill-formed recursive proofs.
  • For induction scheme definitions mutual recursion does not matter, as types that would produce mutual recursive induction schemes contain non strictly positive occurrences and are not valid types in Coq.

    Inductive Foo (a : Type) : Type := F : Bar (Foo a) -> Foo a
    with Bar (a : Type) : Type := B : Foo a -> Bar a.

• The search depth for recursion is limited.
  • The serach depth is limited by the value of maxDepth which is currently set to 1. This means that an induction hypothesis for a type T will only be generated for a constructor argument, if the constructor argument has type T (depth 0) or the constructor argument has type TCon a_1 ... a_n and a_i = T for some i.
    The reason for this limitation is the time Coq needs to verify that the fixpoint proof of an induction scheme is well-formed.
  • This also limits the depth were recursive occurrences can be handled by the ForT and InT properties, as the proof of the ForT_forall lemma is build on an induction over T and needs a induction hypothesis to handle those recursive occurrences.

The generation of those properties, induction schemes and forall lemmas is fully implemented but the proofs of the induction schemes and forall lemmas are not safe to always succeed and need further work. E.g. the unpacking of complex For properties of the induction hypotheses in the proofs of induction schemes does not reach deeply enough and therefore the proof of the induction scheme for Bar fails in the following example.

data Foo a = F [a]
data Bar a = B (Foo (Bar a))

This is especially a problem because at the point in the proof, where the unpacking of ForFoo is not generalized enough and fails, the goal can be 'solved' by applying fixpoint hypothesis. This however means that auto will do exactly that, no matter which hints are given in the hint database, and produce an ill-formed recursive proof. To solve this problem, the generated hints have to get more complex and need more tactics to be referenced directly in the hint instead of relying on auto.