Permalink
Browse files

Bus time

  • Loading branch information...
braibant committed Feb 11, 2013
1 parent 22a393e commit d44e9923a648ed7f0edaec067ee0dba2e43d7770
Showing with 22 additions and 49 deletions.
  1. +4 −3 invert.ml4
  2. +18 −46 test-1.v
View
@@ -33,7 +33,6 @@ let cps_mk_letin
Tacticals.tclTHEN letin (k (Term.mkVar name)) goal
-
let assert_vector
(c: Term.constr array) (* vector of the types of each sub-goal *)
(k : Names.identifier array -> Proof_type.tactic)
@@ -132,7 +131,7 @@ 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.MatchStyle in
+ let case_info = Inductiveops.make_case_info env ind Term.RegularStyle in
begin match constr_list with
| [t] ->
@@ -151,7 +150,9 @@ let invert h gl =
(Term.mkApp (diag, c.Inductiveops.cs_concl_realargs))
ctx
in
- let body subgoal = subgoal
+ 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 *)
in
View
@@ -31,50 +31,22 @@ Lemma l1 : forall n, even (2 + n) -> even n.
| even_SS n x => _
end); simpl.
Restart.
- intros.
- refine
- ( let diag := (fun x : nat =>
- match x return Prop with
- | O => even x
- | S x0 =>
- match x0 return Prop with
- | O => even x0
- | S x1 => even x1
- end
- end)
- in
- match
- H in (even args)
- return (diag args)
-
- with
- | even_0 => _ : diag 0
- | even_SS n x =>
- _ : diag (S (S n))
- end); simpl. constructor. auto.
-Qed.
-
- invert H.
-
- Grab Existential Variables.
- simpl. auto.
+ refine (
+ (fun (n : nat) (H : even (plus (S (S O)) n)) =>
+ let diag :=
+ fun x : nat =>
+ match x return Prop with
+ | O => even x
+ | S x0 => match x0 return Prop with
+ | O => even x0
+ | S x1 => even x1
+ end
+ end in
+
+ match H in (even args) return (diag args) with
+ | even_0 => _
+ | even_SS x x0 => _
+ end)).
simpl. constructor.
-Abort.
-
- Restart.
- intros.
- refine (let diag :=
- fun x : nat =>
- match x return Prop with
- | O => even x
- | S x0 =>
- match x0 return Prop with
- | O => even x0
- | S x1 => even x1
- end
- end in
- match H in (even args) return (diag args) with
- | even_0 => _:diag O
- | even_SS n x => _:diag (S (S n))
- end).
- apply even_0. simpl. auto.
+ simpl. auto.
+Qed.

0 comments on commit d44e992

Please sign in to comment.