No title

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)

DECLARE PLUGIN "constructors"

open Vars
open Term
open Names
open Proofview.Goal
open Environ
open Loc
open Termops
open Inductiveops


let indscheme =
  let open Sigma in
  Proofview.Goal.nf_enter { enter = begin fun gl ->
    let env = Proofview.Goal.env gl in
    let concl = Proofview.Goal.concl gl in
    let (ctx, concl') = decompose_prod_n_assum 3 concl in
    let ((_, ih2_ty) :: (_, ih1_ty) :: (_, p_ty) :: nil) = assums_of_rel_context ctx in
    let (_, n_ty, _) = destProd concl' in
    let n_ind, _ = destInd n_ty in
    Refine.refine { run = begin fun sigma ->
      let fixp_ty = mkProd (Anonymous, n_ty, mkApp (mkRel 4, [|mkRel 1|])) in
      let fixp_ty' = mkProd (Anonymous, n_ty, mkApp (mkRel 5, [|mkRel 1|])) in
      let env' = push_rel (LocalAssum (Anonymous, fixp_ty)) (push_rel_context ctx env) in
      let env'' = push_rel (LocalAssum (Anonymous, n_ty)) env' in
      let caseInfo = make_case_info env'' n_ind MatchStyle in
      let case = mkCase (caseInfo,
                         mkLambda (
                             Anonymous, n_ty,
                             mkApp (mkRel 6, [|mkRel 1|])),
                         mkRel 1,
                         [|mkRel 4;
                           mkLambda (Anonymous, n_ty, mkApp (mkRel 4, [|mkRel 1;mkApp (mkRel 3, [|mkRel 1|])|]))
                         |]) in
      let r = mkLambda(
                  Anonymous, p_ty,
                  mkLambda(
                      Anonymous, ih1_ty,
                      mkLambda(
                          Anonymous, ih2_ty,
                          mkFix (([|0|],0),
                                 ([|Anonymous|], [|fixp_ty|],
                                  [|mkLambda (Anonymous, n_ty, case)|]))))) in
      Sigma (r, sigma, refl)
    end }
  end }

TACTIC EXTEND indscheme
| ["indscheme" ] -> [ indscheme ]
END