Commit b20b6026 authored by Michael Sammler's avatar Michael Sammler
Browse files

bail out early for trivial hyps

parent a150e592
Pipeline #57153 passed with stage
in 12 minutes and 22 seconds
...@@ -63,6 +63,20 @@ Ltac get_head e := ...@@ -63,6 +63,20 @@ Ltac get_head e :=
| _ => constr:(e) | _ => constr:(e)
end. end.
(** A version of done that does not exploit False and contradictions. *)
Ltac done_no_false :=
solve
[ repeat first
[ fast_done
| solve [trivial]
(* All the tactics below will introduce themselves anyway, or make no sense
for goals of product type. So this is a good place for us to do it. *)
| progress intros
| solve [symmetry; trivial]
| solve [apply not_symmetry; trivial]
| split ]
].
(* Checks that a term is closed using a trick by Jason Gross. *) (* Checks that a term is closed using a trick by Jason Gross. *)
Ltac check_closed t := Ltac check_closed t :=
assert_succeeds ( assert_succeeds (
......
...@@ -592,6 +592,9 @@ Ltac liImpl := ...@@ -592,6 +592,9 @@ Ltac liImpl :=
| |- ?P -> ?Q => | |- ?P -> ?Q =>
lazymatch type of P with lazymatch type of P with
| Prop => first [ | Prop => first [
(* first check if the hyp is trivial *)
assert_succeeds (assert (P) as _;[done_no_false|]); intros _
|
progress normalize_goal_impl; simpl progress normalize_goal_impl; simpl
| |
(* (*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment