Permalink
Browse files

Still the same error, about the eliminatin being ill-formed

  • Loading branch information...
1 parent d44e992 commit 6bb35ccf34d91001e1bd0d7895d571a697e31d8a @braibant committed Feb 11, 2013
Showing with 24 additions and 15 deletions.
  1. +18 −11 invert.ml4
  2. +6 −4 test-1.v → test.v
View
@@ -61,7 +61,7 @@ let rec diag sigma env t (a: Term.constr) b return =
tty
(fun x ->
let (ind, args) = Inductive.find_inductive env tty in
- let case_info = Inductiveops.make_case_info env ind Term.MatchStyle in
+ let case_info = Inductiveops.make_case_info env ind Term.RegularStyle in
(* the type of each constructor *)
let (branches_type: Term.types array) = Inductiveops.arities_of_constructors env ind in
try
@@ -130,17 +130,14 @@ let invert h gl =
(* 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.RegularStyle in
begin match constr_list with
| [t] ->
let ind_ty = (Inductiveops.type_of_inductive env ind) in
let arity, sort = Term.destArity ind_ty in
let ind_family = Inductiveops.make_ind_family (ind,[]) in
let constructors = Inductiveops.get_constructors env ind_family in
-
- let diag = diag sigma env t (Term.mkInd ind) (Term.mkInd ind) (Term.mkSort sort) in
+ let diag = diag sigma env t (Term.mkInd ind) (Term.mkInd ind) (Term.mkSort sort) in
let branches diag =
Array.map
(fun c ->
@@ -150,11 +147,18 @@ let invert h gl =
(Term.mkApp (diag, c.Inductiveops.cs_concl_realargs))
ctx
in
+ let _ = Format.printf "concl-ty: %a\n" pp_constr concl_ty in
let body subgoal =
- Term.mkApp (subgoal, c.Inductiveops.cs_args)
- (* Term.mkCast (subgoal, Term.DEFAULTcast, concl_ty) *)
- (* Termops.it_mkLambda_or_LetIn *)
- (* (Term.mkCast (subgoal, Term.DEFAULTcast,concl_ty)) c.Inductiveops.cs_args *)
+ let x =
+ Namegen.it_mkLambda_or_LetIn_name env
+ (Term.mkApp (subgoal, Termops.extended_rel_vect 0 ctx))
+ ctx
+ in
+ Format.printf "subgoal: %a\n" pp_constr x;
+ x
+ (* Termops.it_mkLambda_or_LetIn *)
+ (* (Term.mkCast (subgoal, Term.DEFAULTcast, concl_ty)) *)
+ (* (Term.mkCast (subgoal, Term.DEFAULTcast,concl_ty)) c.Inductiveops.cs_args *)
in
(concl_ty, body)
)
@@ -183,7 +187,10 @@ let invert h gl =
let branches = branches diag in
assert_vector
(Array.map fst branches)
- (fun vect ->
+ (fun vect gl ->
+ let env = Tacmach.pf_env gl in
+ (* extra information for the match *)
+ let case_info = Inductiveops.make_case_info env ind Term.RegularStyle in
let term =
Term.mkCase
(case_info,
@@ -197,7 +204,7 @@ let invert h gl =
)
in
Format.printf "proof term: %a\n" pp_constr term;
- Tactics.refine term
+ Tactics.refine term gl
)
) gl
| _ -> assert false
View
@@ -1,12 +1,12 @@
-Inductive even : nat -> Prop :=
+Inductive even : nat -> Type :=
| even_0 : even 0
| even_SS : forall n, even n -> even (S (S n)).
Declare ML Module "invert".
Lemma l1 : forall n, even (2 + n) -> even n.
intros. Set Printing All.
set (diag := fun x =>
- match x return Prop with
+ match x return Type with
| S (S x1) => even x1
| _ => even x
end).
@@ -20,17 +20,19 @@ Lemma l1 : forall n, even (2 + n) -> even n.
Restart.
intros.
set (diag := fun x =>
- match x return Prop with
+ match x return Type with
| S (S x1) => even x1
| _ => even n
end).
-
refine (match H in even args return diag args
with
| even_0 => _
| even_SS n x => _
end); simpl.
Restart.
+ intros.
+ intros. invert H. simpl. constructor. simpl; intros; auto. Show Proof.
+Qed.
refine (
(fun (n : nat) (H : even (plus (S (S O)) n)) =>
let diag :=

0 comments on commit 6bb35cc

Please sign in to comment.