Generate enhanced induction schemes #159
Description
Description
The induction schemes generated by the compiler should introduces induction hypotheses also for 'hidden' recursive arguments.
Consider the following haskell definitions.
data TreeP a
= LeafP a
| BranchP (TreeP a, TreeP a)
data TreeL a
= LeafL a
| BranchL [TreeP a]The generated induction schemes should produce an induction hypothesis for the branch case, that the trees included in the pair or list fulfill the property that the induction tries to prove.
We might need to define a custom property for each data type, stating that a certain proposition holds for all included values, to formulate such an induction hypothesis. In this case we would need this property for Pair and List respectively. It should look somewhat like the ForFree property.
Also the proving tactic prove_ind has to be adjusted to handle those induction hypotheses.
Motivation
The induction schemes, that are generated with the method introduced by #156, do not include any induction hypothesis for the branch case (x3) as there is no direct recursion. Therefore those two induction schemes are not helpful in a proof.
(* Induction scheme for TreeP *)
Definition TreeP_Ind (Shape : Type) (Pos : Shape -> Type) (a : Type)
(x : TreeP Shape Pos a -> Prop)
(x1 : forall (x0 : Free Shape Pos a), x (leafP x0))
(x3 : forall (x2 : Free Shape Pos (Pair Shape Pos (TreeP Shape Pos a) (TreeP Shape Pos a))), x (branchP x2))
: forall (x4 : TreeP Shape Pos a), x x4.
Proof.
fix H 1; intro; prove_ind.
Defined.
(* Induction scheme for TreeL *)
Definition TreeL_Ind (Shape : Type) (Pos : Shape -> Type) (a : Type)
(x : TreeL Shape Pos a -> Prop)
(x1 : forall (x0 : Free Shape Pos a), x (leafL x0))
(x3 : forall (x2 : Free Shape Pos (List Shape Pos (TreeP Shape Pos a))), x (branchL x2))
: forall (x4 : TreeL Shape Pos a), x x4.
Proof.
fix H 1; intro; prove_ind.
Defined.