Library LambdaTamer.Tactics
Require Import LambdaTamer.Ext.
Require Import LambdaTamer.Binding.
Hint Extern 1 ((fun x => _) = (fun y => _)) =>
apply ext_eq; intro.
Ltac equation_tac simplifier :=
simpl; intuition; repeat progress (simplifier; simpl in *; unfold eq_rect_r in *; simpl in *);
repeat match goal with
| [ H : _ |- _ ] => rewrite H
end;
eauto 6.
Ltac smash' inster :=
match goal with
| [ H : ex _ |- _ ] => destruct H; intuition
| [ H : ?T -> _ |- _ ] =>
match type of T with
| Prop => idtac
end;
let pf := fresh "pf" in
(assert (pf : T);
[eauto; fail
| generalize (H pf); clear H pf; intro H])
| [ H : forall (s : ?T), _ |- _ ] =>
inster T ltac:(fun x => (generalize (H x); clear H; intro H))
| [ |- context[fun x : ?T => ?E x] ] =>
replace (fun x : T => E x) with E;
[idtac
| apply ext_eq; intro; reflexivity]
end.
Ltac default_inster T k :=
match goal with
| [ x : _ |- _ ] => k x
| [ |- context[?E] ] => k E
| [ H' : context[?E] |- _ ] =>
match type of H' with
| _ = _ => k E
end
end.
Ltac stricter_inster T k :=
match T with
| Set =>
match goal with
| [ x : Set |- _ ] => k x
end;
fail 1
| _ =>
match goal with
| [ x : _, s : _ |- _ ] => k (SCons _ x s)
| [ H : context[?E], s : _ |- _ ] => k (SCons _ E s)
| [ H : context[?E] |- _ ] => k E
| _ => default_inster T k
end
end.
Ltac smash inster := repeat smash' inster; intuition eauto.
Ltac lr_tac' inster simplifier :=
repeat progress (simplifier; simpl in *; unfold eq_rect_r in *; simpl in *; smash inster);
repeat (match goal with
| [ |- exists x : ?T, _ ] => inster T ltac:(fun x => exists x)
end; intuition);
repeat match goal with
| [ H : _ |- _ ] => rewrite H
end;
smash inster.
Ltac var_adder val_lr :=
repeat match goal with
| [ v : Var ?G ?t |- _ ] =>
match goal with
| [ H : val_lr _ (VarDenote v _) _ |- _ ] => fail 1
| [ H : _ |- _ ] => generalize (Subst_lr_Var v H); intro
end
end.
Ltac var_adder_two val_lr :=
repeat match goal with
| [ v : Var ?G ?t |- _ ] =>
match goal with
| [ H : val_lr _ _ (VarDenote v _) _ |- _ ] => fail 1
| [ H : _ |- _ ] => generalize (Subst_lr_Var v H); intro
end
end.
Ltac lr_tacN n adder inster simplifier :=
match n with
| O => idtac
| S ?n' =>
lr_tac' inster simplifier;
adder;
lr_tacN n' adder inster simplifier
end.
Ltac lr_tac := lr_tacN 2.
Hint Extern 1 (Binding.Subst_lr _ ?val_lr (SCons ?dom ?xp _) (SCons _ ?xo _)) =>
match goal with
| [ H1 : val_lr _ _ _, H0 : _ |- _ ] =>
generalize (Slr_Cons dom xp xo H1 H0); trivial; fail
end.
Index
This page has been generated by coqdoc