Require Export Undecidability.TM.Code.CodeTM Undecidability.TM.Code.Copy Undecidability.TM.Code.ChangeAlphabet Undecidability.TM.Code.WriteValue.
Require Export Undecidability.TM.Compound.TMTac.
Require Export Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi.
Require Import Lia.
Export Set Default Proof Using "Type".
Ltac clear_tape_eqs :=
repeat once lazymatch goal with
| [ H: ?t'[@ ?x] = ?t[@ ?x] |- _ ] => clear H
end.
Tactic Notation "destruct" "_" "in" constr(H):=
match type of H with
| context[match ?X with _ => _ end] => destruct X
| context[match ?X with _ => _ end] => destruct X
end.
Tactic Notation "tacInEvar" constr(E) tactic3(tac) :=
is_evar E;
let t := type of E in
let __tmp_callInEvar := fresh "__tmp_callInEvar" in
evar (__tmp_callInEvar:t);
(only [__tmp_callInEvar]:tac);unify E __tmp_callInEvar;subst __tmp_callInEvar;instantiate.
Tactic Notation "introsSwitch" ne_simple_intropattern_list(P):=
once lazymatch goal with
|- (forall f' , ?REL _ (?Rmove f')) =>
tacInEvar Rmove intros P;cbn beta;intros P
end.
Tactic Notation "destructBoth" constr(g) "as" simple_intropattern(P) :=
once lazymatch goal with
|- (RealiseIn _ ?Rmove _) =>
tacInEvar Rmove (destruct g as P);destruct g as P;cbn zeta iota beta
| |- (?REL _ ?Rmove) =>
tacInEvar Rmove (destruct g as P);destruct g as P;cbn zeta iota beta
end.
Tactic Notation "destructBoth" constr(g) :=
destructBoth g as [].
Tactic Notation "infTer" int_or_var(n) :=
let t := try (first
[match goal with
|- exists x:_,_ => simple notypeclasses refine (@ex_intro _ _ _ _);[shelve|cbn beta]
end
| simple apply conj | simple eapply Nat.le_refl])
in t;do n t.
Tactic Notation "length_not_eq" "in" constr(H):=
let H' := fresh "H" in
specialize (f_equal (@length _) H) as H';repeat (try autorewrite with list in H';cbn in H');nia.
Ltac length_not_eq :=
let H := fresh "H" in intros H;exfalso;length_not_eq in H.
Ltac specializeFin H' :=
match type of H' with
forall i : Fin.t ?n, _ => do_n_times_fin n ltac:(fun i => let H := fresh H' in specialize (H' i) as H;cbn in H)
end.
From Coq.ssr Require ssrfun.
Module Option := ssrfun.Option.
Require Export Undecidability.TM.Compound.TMTac.
Require Export Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi.
Require Import Lia.
Export Set Default Proof Using "Type".
Ltac clear_tape_eqs :=
repeat once lazymatch goal with
| [ H: ?t'[@ ?x] = ?t[@ ?x] |- _ ] => clear H
end.
Tactic Notation "destruct" "_" "in" constr(H):=
match type of H with
| context[match ?X with _ => _ end] => destruct X
| context[match ?X with _ => _ end] => destruct X
end.
Tactic Notation "tacInEvar" constr(E) tactic3(tac) :=
is_evar E;
let t := type of E in
let __tmp_callInEvar := fresh "__tmp_callInEvar" in
evar (__tmp_callInEvar:t);
(only [__tmp_callInEvar]:tac);unify E __tmp_callInEvar;subst __tmp_callInEvar;instantiate.
Tactic Notation "introsSwitch" ne_simple_intropattern_list(P):=
once lazymatch goal with
|- (forall f' , ?REL _ (?Rmove f')) =>
tacInEvar Rmove intros P;cbn beta;intros P
end.
Tactic Notation "destructBoth" constr(g) "as" simple_intropattern(P) :=
once lazymatch goal with
|- (RealiseIn _ ?Rmove _) =>
tacInEvar Rmove (destruct g as P);destruct g as P;cbn zeta iota beta
| |- (?REL _ ?Rmove) =>
tacInEvar Rmove (destruct g as P);destruct g as P;cbn zeta iota beta
end.
Tactic Notation "destructBoth" constr(g) :=
destructBoth g as [].
Tactic Notation "infTer" int_or_var(n) :=
let t := try (first
[match goal with
|- exists x:_,_ => simple notypeclasses refine (@ex_intro _ _ _ _);[shelve|cbn beta]
end
| simple apply conj | simple eapply Nat.le_refl])
in t;do n t.
Tactic Notation "length_not_eq" "in" constr(H):=
let H' := fresh "H" in
specialize (f_equal (@length _) H) as H';repeat (try autorewrite with list in H';cbn in H');nia.
Ltac length_not_eq :=
let H := fresh "H" in intros H;exfalso;length_not_eq in H.
Ltac specializeFin H' :=
match type of H' with
forall i : Fin.t ?n, _ => do_n_times_fin n ltac:(fun i => let H := fresh H' in specialize (H' i) as H;cbn in H)
end.
From Coq.ssr Require ssrfun.
Module Option := ssrfun.Option.