Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.

No title

(*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