Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Une version qui marche pour les cas simples

  • Loading branch information...
commit f7143e85946ed278df50e6ad7c824574bed41a72 1 parent 8b5b2be
@braibant authored
Showing with 49 additions and 25 deletions.
  1. +14 −6 invert.ml4
  2. +35 −19 test.v
View
20 invert.ml4
@@ -24,17 +24,18 @@ let nowhere =
let cps_mk_letin
(name:string)
(c: Term.constr)
- (k : Term.constr -> Proof_type.tactic)
+ (k : Names.identifier -> Proof_type.tactic)
: Proof_type.tactic =
fun goal ->
let name = (Names.id_of_string name) in
let name = Tactics.fresh_id [] name goal in
let letin = (Tactics.letin_tac None (Names.Name name) c None nowhere) in
- Tacticals.tclTHEN letin (k (Term.mkVar name)) goal
+ Tacticals.tclTHEN letin (k name) goal
let assert_vector
(c: Term.constr array) (* vector of the types of each sub-goal *)
+ subtac
(k : Names.identifier array -> Proof_type.tactic)
: Proof_type.tactic =
let rec aux i l =
@@ -46,7 +47,8 @@ let assert_vector
let name = Tactics.fresh_id [] name goal in
let t = (Tactics.assert_tac (Names.Name name) c.(i)) in
let _ = Format.printf "subgoal %i: %a\n" i pp_constr c.(i) in
- Tacticals.tclTHENS t [Tacticals.tclIDTAC; (aux (succ i) (name :: l))] goal
+ Tacticals.tclTHENS t [ Tacticals.tclTHEN (Tactics.clear l) subtac;
+ aux (succ i) (name :: l)] goal
in
aux 0 []
@@ -172,7 +174,7 @@ let invert h gl =
mk_fun (!! "args") args_ty
(fun args ->
(* the [as] part *)
- mk_fun (!! "as_x") h_ty
+ mk_fun (!! "as_x") (Term.mkApp (Term.mkInd ind, [| Term.mkVar args |]))
(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'] *)
@@ -184,17 +186,23 @@ let invert h gl =
in
cps_mk_letin "diag" diag
(fun diag ->
- let branches = branches diag in
+ let branches = branches (Term.mkVar diag) in
assert_vector
(Array.map fst branches)
+ (
+ Tacticals.tclTHENLIST
+ [Tactics.unfold_constr (Libnames.VarRef diag);
+ Tactics.clear [diag; h]
+ ])
(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 _ = Format.printf "return clause: %a\n" pp_constr (return_clause (Term.mkVar diag)) in
let term =
Term.mkCase
(case_info,
- return_clause diag,
+ return_clause (Term.mkVar diag),
Term.mkVar h,
Array.mapi
(
View
54 test.v
@@ -31,24 +31,40 @@ Lemma l1 : forall n, even (2 + n) -> even n.
end); simpl.
Restart.
intros.
- intros. invert H. simpl. constructor. simpl; intros; auto. Show Proof.
+ invert H. constructor. intros; auto. Show Proof.
Qed.
- 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.
- simpl. auto.
+
+
+Inductive mul3 : nat -> Prop :=
+ | T0 : mul3 0
+ | T3: forall n, mul3 n -> mul3 (3 + n).
+
+Lemma inv_mul_3plusn : forall n, mul3 (3 + n) -> mul3 n.
+Proof.
+intros n m.
+invert m. constructor.
+simpl. auto.
Qed.
+
+(* Not in the paper: version without 0 *)
+Lemma inv_mul_3plusn_no0 : forall n, mul3 (3 + n) -> mul3 n.
+Proof.
+intros n m.
+invert m.
+constructor.
+simpl. auto.
+Qed.
+
+
+
+Section sec_absu_2ismul3.
+
+Variable C: Prop.
+
+Lemma absurd2_inv : mul3 2 -> C.
+Proof.
+intros H.
+(* invert H. *)
+Abort.
+
+End sec_absu_2ismul3.
Please sign in to comment.
Something went wrong with that request. Please try again.