Permalink
Browse files

Incorrect elimination of H in the inductive type "even"

  • Loading branch information...
1 parent 9d791e7 commit f93ba9c262e2e8ab295032988213da5cb89d0bf7 @braibant committed Feb 11, 2013
Showing with 144 additions and 39 deletions.
  1. +144 −39 invert.ml4
View
@@ -9,57 +9,162 @@ let mk_fun
(k : Names.identifier -> Term.constr) =
Term.mkNamedLambda name t (Term.subst_vars [name] (k name))
+let mk_let
+ (name:Names.identifier)
+ (c: Term.constr)
+ (t: Term.constr)
+ (k : Names.identifier -> Term.constr) =
+ Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name))
+
+(* constructs the term fun x => match x with | t => a | _ => b end
+ assume that t is in head normal form *)
+let rec diag sigma env t (a: Term.constr) b =
+ let tty = Typing.type_of env sigma t in
+ let t = Tacred.hnf_constr env sigma t in
+ let _ = Format.printf "diag %a %a %a\n" pp_constr t pp_constr a pp_constr b in
+ mk_fun
+ (Names.id_of_string "x")
+ tty
+ (fun x ->
+ let (ind, args) = Inductive.find_inductive env tty in
+ let case_info = Inductiveops.make_case_info env ind Term.MatchStyle in
+ (* the type of each constructor *)
+ let (branches_type: Term.types array) = Inductiveops.arities_of_constructors env ind in
+ try
+ let head_t, args_t =
+ match Term.kind_of_term t with
+ | Term.App(hd, v) ->
+ (match Term.kind_of_term hd with
+ | Term.Construct c' -> c',v
+ )
+ | Term.Construct c' -> c', [||]
+ in
+ let branches = Array.mapi
+ (fun i ty ->
+ let (args_ty,concl_ty) = Term.decompose_prod_assum ty in
+ let args_ty' = List.rev args_ty in
+ if i + 1 = snd head_t
+ then
+ (* in this case, we continue to match on [t] *)
+ begin
+ let env = (Environ.push_rel_context args_ty env) in
+ (* we must match each of the arguments of the constructor
+ against the corresponding term in the arguments of t *)
+ let rec aux k : Term.constr=
+ if k = Array.length args_t
+ then
+ a
+ else
+ diag sigma env
+ args_t.(k)
+ (aux (succ k))
+ b
+ in
+ aux 0
+ end
+ else
+ (* otherwise, in the underscore case, we return [b] *)
+ Termops.it_mkLambda_or_LetIn b args_ty
+ )
+ branches_type
+ in
+ let return =
+ let context =
+ (Names.Anonymous, None, tty) ::
+ List.map (fun t -> Names.Anonymous, None, Typing.type_of env sigma t) (List.rev args)
+ in
+ Termops.it_mkLambda_or_LetIn
+ (
+ Typing.type_of env sigma b
+ ) context
+ in Term.mkCase (case_info,return,Term.mkVar x, branches)
+ with
+ | _ -> Term.mkApp (a, [|Term.mkVar x|])
+ )
+;;
+
+
let invert h gl =
let env = Tacmach.pf_env gl in
+ let sigma = Tacmach.project gl in
let concl = Tacmach.pf_concl gl in
let h_ty = Tacmach.pf_get_hyp_typ gl h in
+ (** ensures that the name x is fresh in the _first_ goal *)
let (!!) x = Tactics.fresh_id [] ((Names.id_of_string x)) gl in
(* get the name of the inductive and the list of arguments it is applied to *)
let (ind, constr_list) = Inductive.find_inductive env h_ty in
(* extra information for the match *)
let case_info = Inductiveops.make_case_info env ind Term.MatchStyle in
- (* return clause: for now, it is just the dummy return clause that
- returns the conclusion of the goal *)
- let (return_clause: Term.constr) =
- begin
- mk_fun (!! "args") (Inductiveops.type_of_inductive env ind)
- (fun args ->
- mk_fun (!! "as_x") h_ty
- (fun x ->
- concl
- )
- )
- end
- in
- (* the type of each constructors *)
- let (branches_type: Term.types array) = Inductiveops.arities_of_constructors env ind in
+ begin match constr_list with
+ | [t] ->
+ (* return clause *)
+ let return_clause diag =
+ begin
+ let ind_ty = (Inductiveops.type_of_inductive env ind) in
+ let arity, sort = Term.destArity ind_ty in
+ let _ = assert (List.length arity = 1) in (* for now *)
+ let (_,_,args_ty) = List.hd arity in
+ (* the [in] part *)
+ mk_fun (!! "args") args_ty
+ (fun args ->
+ (* the [as] part *)
+ mk_fun (!! "as_x") h_ty
+ (fun x ->
+ (* for instance if the conclusion is [even n] and the
+ inductive is [even n'], we can substitute [n] in the goal with [n'] *)
+ Term.mkApp (Term.mkVar diag, [|Term.mkVar args|])
+ )
+ )
+ end
+ in
+
+ (* the type of each constructors *)
+ let (branches_type: Term.types array) = Inductiveops.arities_of_constructors env ind in
+
+ (* each branch must be presented as \args.term *)
+ let sigma = ref sigma in
+ let branches =
+ let branches = Array.map
+ (fun ty ->
+ (* we decompose the type of this particular constructor *)
+ let (args_ty,concl_ty) = Term.decompose_prod_assum ty in
+ let env = (Environ.push_rel_context args_ty env) in
+ let subgoal = Evarutil.e_new_evar sigma env concl in
+ Termops.it_mkLambda_or_LetIn (subgoal) args_ty
+ ) branches_type in
+ branches
+ in
+ Tacticals.tclTHEN
+ (Refiner.tclEVARS !sigma)
+ (fun gl ->
+ (* the proof term *)
+ let term =
+ begin
+ let env = Tacmach.pf_env gl in
+ let sigma = Tacmach.project gl in
+ let diag = (diag sigma env t (Term.mkInd ind) h_ty) in
+ mk_let
+ (!! "diag")
+ diag
+ (Typing.type_of env sigma diag)
+ (fun diag ->
+ Term.mkCase (case_info,return_clause diag, Term.mkVar h, branches) )
+ end
+ in
+ (
+ Format.printf "%a\n" pp_constrs constr_list;
+ Format.printf "%a\n%!" pp_constr term;
+ Tactics.refine term gl
+ )
+ ) gl
- (* each branch must be presented as \args.term *)
- let evar_map, branches =
- let evar_map = ref (Tacmach.project gl) in
- let branches = Array.map
- (fun ty ->
- let (args_ty,concl_ty) = Term.decompose_prod_assum ty in
- let env = Environ.push_rel_context args_ty env in
- let evar_map', sub_goal = Evarutil.new_evar !evar_map env concl_ty in
- evar_map := evar_map';
- Termops.it_mkLambda_or_LetIn (sub_goal) args_ty
- ) branches_type in
- !evar_map, branches
- in
- Tacticals.tclTHEN
- (Refiner.tclEVARS evar_map)
- (fun gl ->
- (* the proof term *)
- let term = Term.mkCase (case_info,return_clause, Term.mkVar h, branches) in
- Format.printf "%a\n" pp_constrs constr_list;
- Format.printf "%a\n%!" pp_constr term;
- Tactics.refine term gl
- ) gl
+ | _ -> assert false
+ end
+;;
open Tacmach
open Tacticals
@@ -70,5 +175,5 @@ open Genarg
TACTIC EXTEND invert
- | ["invert" ident(h)] -> [invert h]
- END;;
+| ["invert" ident(h)] -> [invert h]
+ END;;

0 comments on commit f93ba9c

Please sign in to comment.