Add generation of enhanced induction schemes

base/Prelude.toml

@@ -208,14 +208,17 @@ exported-values = [
 ##############################################################################
 
 [[types]]
-  haskell-name = 'Prelude.([])'
-  coq-name     = 'List'
-  agda-name    = 'List'
-  arity        = 1
-  cons-names   = [
+  haskell-name          = 'Prelude.([])'
+  coq-name              = 'List'
+  agda-name             = 'List'
+  arity                 = 1
+  cons-names            = [
       'Prelude.([])',
       'Prelude.(:)',
     ]
+  coq-for-property-name = 'ForList'
+  coq-in-property-names = ['InList']
+  coq-forall-lemma-name = 'ForList_forall'
 
 [[constructors]]
   haskell-type    = 'Prelude.([]) a'
@@ -240,11 +243,17 @@ exported-values = [
 ##############################################################################
 
 [[types]]
-  haskell-name = 'Prelude.(,)'
-  coq-name     = 'Pair'
-  agda-name    = 'Pair'
-  arity        = 2
-  cons-names   = ['Prelude.(,)']
+  haskell-name          = 'Prelude.(,)'
+  coq-name              = 'Pair'
+  agda-name             = 'Pair'
+  arity                 = 2
+  cons-names            = ['Prelude.(,)']
+  coq-for-property-name = 'ForPair'
+  coq-in-property-names = [
+      'InPair_1',
+      'InPair_2'
+    ]
+  coq-forall-lemma-name = 'ForPair_forall'
 
 [[constructors]]
   haskell-type    = 'a -> b -> Prelude.(,) a b'

base/coq/Free.v

@@ -4,4 +4,5 @@ From Base Require Export Free.Induction.
 From Base Require Export Free.Malias.
 From Base Require Export Free.Monad.
 From Base Require Export Free.Tactic.ProveInd.
+From Base Require Export Free.Tactic.ProveForall.
 From Base Require Export Free.Tactic.Simplify.

base/coq/Free/Tactic/ProveForall.v

@@ -0,0 +1,121 @@
+(* This file contains the tactic [prove_forall] that proofs such a the
+   [ForallT_forall] lemmas for datatypes.
+   For each datatype [T] that has type variables, there should be the inductive
+   property [ForT] and for every tpe variable of that type a Property [InT_a]. 
+   The lemma [ForT_forall] that states the connection between those properties.
+*)
+
+From Base Require Import Free.ForFree.
+
+Require Import Coq.Program.Equality.
+
+(* This is the hint database which is used by [prove_forall]. *)
+Create HintDb prove_forall_db.
+
+(* This tactic splits all hypotheses, which are conjunctions, into smaller
+   hypotheses. *)
+Ltac prove_forall_split_hypotheses :=
+  repeat (match goal with
+          | [H : _ /\ _ |- _] => destruct H
+          end).
+
+(* This tactic rewrites a 'ForT' hypothesis [HF] using a forall lemma
+   [forType_forall] and specializes it using a value [x] for which an 'InT'
+   hypothesis [IF] exists.
+   This tactic should be instantiated for types with type variables and added to
+   [prove_forall_db]. *)
+Ltac prove_forall_ForType_InType HF HI x forType_forall :=
+  rewrite forType_forall in HF;
+  prove_forall_split_hypotheses;
+  match goal with
+  | [ HF1 : forall y, _ -> _ |- _ ] =>
+    specialize (HF1 x HI);
+    auto with prove_forall_db
+  end.
+
+(* [prove_forall_ForType_InType] instance of [Free].
+   You can use this as reference for instances of
+   [prove_forall_ForType_InType]. *)
+Hint Extern 0 =>
+  match goal with
+  | [ HF : ForFree _ _ _ _ ?fx
+    , HI : InFree _ _ _ ?x ?fx
+    |- _ ] =>
+      prove_forall_ForType_InType HF HI x ForFree_forall
+  end : prove_forall_db.
+
+(* Rewrites the goal using the given 'forall' lemma.
+   This tactic should be instantiated for types with type variables and added to
+   [prove_forall_db]. *)
+  Ltac prove_forall_prove_ForType forType_forall :=
+  rewrite forType_forall;
+  repeat split;
+  let x  := fresh "x"
+  in let HI := fresh "HI"
+  in intros x HI;
+  auto with prove_forall_db.
+
+(* [prove_forall_prove_ForType] instance of [Free]. *)
+Hint Extern 0 (ForFree _ _ _ _ _) =>
+  prove_forall_prove_ForType ForFree_forall : prove_forall_db.
+
+(* Applies a hypothesis which is an implication with two fulfilled
+   preconditions to prove the goal. *)
+Ltac prove_forall_trivial_imp :=
+  match goal with
+  | [ HImp : ?TF -> ?TI -> ?P
+    , HF : ?TF
+    , HI : ?TI
+    |- ?P ] =>
+    apply (HImp HF HI)
+  end.
+
+Hint Extern 1 => prove_forall_trivial_imp : prove_forall_db.
+
+(* Tries to prove an 'InT' property by using an constructor for that type.
+   This tactic should be instantiated locally with all 'InT' constructors of a
+   type with type variables and added to [prove_forall_db] when proving the
+   corresponding 'forall' lemma. *)
+  Ltac prove_forall_finish_rtl Con :=
+  match goal with
+  | [ H : (forall y, _ -> ?P y) -> _
+    |- _ ] =>
+      apply H;
+      let x  := fresh "x"
+      in let HI := fresh "HI"
+      in intros x HI;
+      auto with prove_forall_db
+  | [ H : forall y, ?TI -> ?P y |- ?P ?x ] =>
+    apply H;
+    eapply Con;
+    eauto
+  end.
+
+Hint Extern 1 => prove_forall_finish_rtl : prove_forall_db.
+
+(* This tactic proves a 'forall' lemma using a given induction scheme for the
+   corresponding type using the database [prove_forall_db].
+   The database should contain an instance of [prove_forall_finish_rtl] for
+   every 'InT' constructor of that type and instances of
+   [prove_forall_ForType_InType] and [prove_forall_prove_ForType] for every
+   dependent type. *)
+Ltac prove_forall type_ind :=
+  let C := fresh "C"
+  in intro C; split;
+  [ let HF := fresh "HF"
+    in intro HF;
+    repeat split;
+    let x  := fresh "x"
+    in let HI := fresh "HI"
+    in intros x HI;
+    induction C using type_ind;
+    dependent destruction HI;
+    dependent destruction HF;
+    auto with prove_forall_db
+  | let H  := fresh "H"
+    in intro H;
+    prove_forall_split_hypotheses;
+    induction C using type_ind;
+    constructor;
+    auto with prove_forall_db
+  ].

base/coq/Free/Tactic/ProveInd.v

@@ -1,41 +1,138 @@
+(* This file contains tactics that help to prove induction schemes for types.
+   [prove_ind] is able to do such a proof if all required instances of
+   [prove_ind_prove_for_type] were added to [prove_ind_db]. *)
+
 From Base Require Import Free.ForFree.
 From Base Require Import Free.Induction.
 From Base Require Import Free.Monad.
 
 Require Import Coq.Program.Equality.
 
-Local Ltac is_fixpoint H P :=
-  match type of H with
-  | forall x, P x => idtac
-  end.
+(* The hint database that contains instances of [prove_ind_prove_for_type]. *)
+Create HintDb prove_ind_db.
 
-Local Ltac prove_ind_apply_assumption :=
+(* Trivial property. *)
+Definition NoProperty {A : Type} : A -> Prop := fun _ => True.
+Hint Extern 0 (NoProperty _) => unfold NoProperty; constructor : prove_ind_db.
+
+(* This tactic is applied at the beginning of the proof of an induction scheme
+   to select the correct hypothesis for the current induction case. *)
+Ltac prove_ind_select_case FP :=
   match goal with
-  | [ H : _ |- ?P ?x ] => tryif is_fixpoint H P then fail else apply H
+  | [ H : ?T |- _ ] =>
+    lazymatch type of FP with
+    | T => fail
+    | _ => apply H; clear H
+    end
   end.
 
-Local Ltac prove_ind_prove_for_free FP :=
+(* This tactic eliminates the monadic layer of an induction hypothesis. *)
+Ltac prove_ind_prove_ForFree :=
   match goal with
-  | [ fx: Free ?Shape ?Pos ?T |- _ ] =>
+  | [ fx : Free ?Shape ?Pos _ |- _ ] =>
     match goal with
-    | [ |- ForFree Shape Pos T ?P fx ] =>
-         let x1    := fresh "x"
-      in let H    := fresh "H"
-      in let x2   := fresh "x"
+    | [ |- ForFree Shape Pos ?T ?P fx ] =>
+      apply ForFree_forall;
+      let x1   := fresh "x"
+      in let H := fresh "H"
+      in intros x1 H;
+      let x2   := fresh "x"
       in let s    := fresh "s"
       in let pf   := fresh "pf"
       in let IHpf := fresh "IHpf"
-      in let p    := fresh "p"
-      in apply ForFree_forall; intros x1 H;
-         induction fx as [ x2 | s pf IHpf ] using Free_Ind;
-         [ inversion H; subst; apply FP
-         | dependent destruction H; subst; destruct H as [ p ];
-           apply (IHpf p); apply H ]
+      in induction fx as [ x2 | s pf IHpf ] using Free_Ind;
+      [ inversion H; subst; clear H
+      | dependent destruction H;
+        match goal with
+        | [ IHpf : forall p : Pos s, InFree Shape Pos T ?x1 (pf p) -> P ?x1
+          , H : exists q : Pos s, InFree Shape Pos T ?x1 (pf q)
+          |- _ ] =>
+          let p := fresh "p"
+          in destruct H as [ p H ];
+             apply (IHpf p H)
+        end ]
+    end
+  end.
+
+(* This tactic tries to finish the proof with a given hypothesis with fulfilled
+  preconditions. *)
+Ltac prove_ind_apply_hypothesis H :=
+  match type of H with
+  | ?PC -> _ =>
+    match goal with
+    | [ H2 : PC |- _ ] => specialize (H H2); prove_ind_apply_hypothesis H
     end
+  | _ => apply H
   end.
 
+Hint Extern 0 => prove_ind_apply_hypothesis : prove_ind_db.
+
+(* This tactic splits all hypotheses, which are conjunctions, into smaller
+   hypotheses. *)
+Ltac prove_ind_split_hypotheses :=
+  repeat (match goal with
+          | [H : _ /\ _ |- _] => destruct H
+          end).
+
+(* This tactic rewrites a 'ForT' hypothesis [HF] using a forall lemma
+   [forType_forall] and specializes it using a value [x] for which an 'InT'
+   hypothesis [IF] exists. *)
+Ltac prove_ind_ForType_InType HF HI x forType_forall :=
+  rewrite forType_forall in HF;
+  prove_ind_split_hypotheses;
+  match goal with
+  | [ HF1 : forall y, _ -> _ |- _ ] =>
+    specialize (HF1 x HI);
+    try (prove_ind_apply_hypothesis HF1)
+  end.
+
+(* This tactic eliminates intermediate monadic layers. *)
+Ltac prove_ind_prove_ForFree_InFree :=
+  match goal with
+  | [ HIF : InFree ?Shape ?Pos ?T ?x ?fx
+    , IH  : ForFree ?Shape ?Pos ?T _ ?fx
+    |- _ ] =>
+    rewrite ForFree_forall in IH;
+    specialize (IH x HIF); clear HIF;
+    try (prove_ind_apply_hypothesis IH)
+  | [ HIF : InFree ?Shape ?Pos ?T ?x ?fx
+    |- ?P ?x ] =>
+    let x1      := fresh "x"
+    in let s    := fresh "s"
+    in let pf   := fresh "pf"
+    in let IHpf := fresh "IHpf"
+    in induction fx as [ x1 | s pf IHpf ] using Free_Ind;
+       [ inversion HIF; subst; clear HIF
+       | dependent destruction HIF;
+         match goal with
+         | [H : exists p : Pos s, InFree Shape Pos T x (pf p) |- _ ] =>
+           let p := fresh "p"
+           in destruct H as [ p H ]; apply (IHpf p H); easy
+         end
+       ]
+  end.
+
+(* Tries to prove a 'ForT' property for [x] by using the given 'forall' lemma
+   and induction scheme.
+   This tactic should be instantiated for types with type variables and added
+   to [prove_ind_db]. *)
+Ltac prove_ind_prove_ForType x forType_forall type_ind :=
+  apply forType_forall;
+  repeat split;
+  induction x using type_ind;
+  let y    := fresh "y"
+  in let H := fresh "H"
+  in intros y H; inversion H; subst; clear H;
+  prove_ind_prove_ForFree_InFree.
+
+(* This tactic proves the induction scheme for a type.
+   It requires the database [prove_ind_db] to contain instances of
+   [prove_ind_prove_ForType] for all dependent types. *)
 Ltac prove_ind :=
   match goal with
   | [ FP : forall y, ?P y |- ?P ?x ] =>
-    destruct x; prove_ind_apply_assumption; prove_ind_prove_for_free FP
+    destruct x;
+    prove_ind_select_case FP;
+    prove_ind_prove_ForFree;
+    auto with prove_ind_db
   end.