Library mcertikos.layerlib.FutureTactic
Require Export ArithLemma.
Require Export ListLemma.
Tactic Notation "on_fun" constr(f) "act" tactic(tac) :=
match goal with
| [H: f _ = _ |- _] ⇒ tac H
| [H: f _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| [H: f _ _ _ _ _ _ _ _ _ _ _ _ = _ |- _] ⇒ tac H
| _ ⇒ fail 1 "Tactic 'on_fun' failed, Cannot find any function application of" f
end.
Tactic Notation "on_type" constr(T) "act" tactic(tac) :=
let H :=
match goal with
| [ H: T |- _ ] ⇒ H
| _ ⇒ fail 1 "Can not find hypothesis with type " T
end
in tac H.
Tactic Notation "on_eq" constr(I) "act" "l:" tactic(ltac) "r:" tactic(rtac) :=
match goal with
| [Hl: I = ?b |- _] ⇒ ltac Hl
| [Hr: ?b = I |- _] ⇒ rtac Hr
| _ ⇒ fail 1 "Can not find hypothesis with type " I " = ..., or ... = " I
end.
Tactic Notation "on_eq_left" constr(I) "act" tactic(tac) :=
match goal with
| [H: I = ?b |- _] ⇒ tac H
| _ ⇒ fail 1 "Cannot find " I " = _"
end.
Tactic Notation "on_eq_right" constr(I) "act" tactic(tac) :=
match goal with
| [H: ?b = I |- _] ⇒ tac H
| _ ⇒ fail 1 "Cannot find _ = " I
end.
Tactic Notation "onleft" tactic(t) :=
match goal with
| [|- (?l < ?r)%nat] ⇒ t l
| [|- (?l ≤ ?r)%nat] ⇒ t l
| [|- (?l = ?r)%nat] ⇒ t l
| [|- (?l ≥ ?r)%nat] ⇒ t l
| [|- (?l > ?r)%nat] ⇒ t l
| [|- le ?l ?r] ⇒ t l
| [|- (?l < ?r)%Z] ⇒ t l
| [|- (?l ≤ ?r)%Z] ⇒ t l
| [|- (?l = ?r)%Z] ⇒ t l
| [|- (?l ≥ ?r)%Z] ⇒ t l
| [|- (?l > ?r)%Z] ⇒ t l
| [|- Zle ?l ?r] ⇒ t l
| [|- @eq _ ?l ?r] ⇒ t l
| _ ⇒ fail "cannot find left side in current goal"
end.
Tactic Notation "onright" tactic(t) :=
match goal with
| [|- (?l < ?r)%nat] ⇒ t r
| [|- (?l ≤ ?r)%nat] ⇒ t r
| [|- (?l = ?r)%nat] ⇒ t r
| [|- (?l ≥ ?r)%nat] ⇒ t r
| [|- (?l > ?r)%nat] ⇒ t r
| [|- (?l < ?r)%Z] ⇒ t r
| [|- (?l ≤ ?r)%Z] ⇒ t r
| [|- (?l = ?r)%Z] ⇒ t r
| [|- (?l ≥ ?r)%Z] ⇒ t r
| [|- (?l > ?r)%Z] ⇒ t r
| [|- @eq _ ?l ?r] ⇒ t r
| _ ⇒ fail "cannot find right side in current goal"
end.
Ltac blast id :=
match goal with
| [H : ?T |- _] ⇒
match H with
| id ⇒
match T with
| ?P1 ∧ ?P2 ⇒
let Hp1 := fresh H in
let Hp2 := fresh H in
destruct H as [Hp1 Hp2]; blast Hp1; blast Hp2
| ex ?e ⇒
let x := fresh "e" in
let Hp := fresh "Hex" in
destruct H as [x Hp]; blast Hp
| ?f ?a = ?f´ ?a´ ⇒ inversion H
| _ ⇒ idtac
end
end
| [H : ?a = ?b |- _] ⇒
match a with
| id ⇒ destruct id; inversion H
end
| [H : ?a = ?b |- _] ⇒
match b with
| id ⇒ destruct id; inversion H
end
| _ ⇒ fail 1 "no hypothesis names" id ", or " id "is not destructable"
end.
Ltac expose_if :=
match goal with
| [|- context [_ || _]] ⇒ unfold orb
| [|- context [orb _ _]] ⇒ unfold orb
| [|- context [_ && _]] ⇒ unfold andb
| [|- context [andb _ _]] ⇒ unfold andb
| [|- context [implb _ _]] ⇒ unfold implb
end.
Ltac if_true :=
repeat expose_if;
match goal with
| [|- context [if proj_sumbool ?d then _ else _]] ⇒ rewrite psum_true; [| apply (true_ex d); try omega]
| [|- context [if zle ?n ?m then _ else _]] ⇒ rewrite zle_true; [| try omega]
| [|- context [if zlt ?n ?m then _ else _]] ⇒ rewrite zlt_true; [| try omega]
| [|- context [if zeq ?n ?m then _ else _]] ⇒ rewrite zeq_true; [| try omega]
| [|- context [if zle_le ?a ?b ?c then _ else _]] ⇒ rewrite zle_le_true; [| try omega]
| [|- context [if ?d then _ else _]] ⇒
match type of d with
| {?p} + {?q} ⇒ rewrite if_dec_true; [| try omega | try omega]
| bool ⇒ rewrite if_bool_true
end
| _ ⇒ fail "cannot find if statememt"
end.
Ltac if_false :=
repeat expose_if;
match goal with
| [|- context [if proj_sumbool ?d then _ else _]] ⇒ rewrite psum_false; [| apply (false_ex d); try omega]
| [|- context [if zle ?n ?m then _ else _]] ⇒ rewrite zle_false; [| try omega]
| [|- context [if zlt ?n ?m then _ else _]] ⇒ rewrite zlt_false; [| try omega]
| [|- context [if zeq ?n ?m then _ else _]] ⇒ rewrite zeq_false; [| try omega]
| [|- context [if ?d then _ else _]] ⇒
match type of d with
| {?p} + {?q} ⇒ rewrite if_dec_false; [| try omega | try omega]
| bool ⇒ rewrite if_bool_false
end
| _ ⇒ fail "cannot find if statememt"
end.
Ltac solve_dec t :=
match type of t with
| {?a} + {?b} ⇒ destruct t; try omega
end.
Ltac solve_bool :=
match goal with
| [|- context [proj_sumbool ?t]] ⇒
solve_dec t;
match goal with
| [|- context [proj_sumbool (left ?a)]] ⇒ rewrite proj_sumbool_left
| [|- context [proj_sumbool (right ?a)]] ⇒ rewrite proj_sumbool_right
end
| [|- context [?t]] ⇒
match type of t with
| {_} + {_} ⇒ solve_dec t
end
end.
Ltac case_cmp_step :=
match goal with
| [|- context [match ?m with _ ⇒ _ end]] ⇒
destruct m; auto
end.
Ltac case_cmp :=
progress repeat case_cmp_step.
Ltac const_nat n :=
let rec checknat_bound b n :=
match b with
| O ⇒ idtac
| S ?b´ ⇒
match n with
| O ⇒ idtac
| S ?n´ ⇒ checknat_bound b´ n´
| _ ⇒ fail 1
end
end in
checknat_bound 16%nat n.
Ltac const_pos n :=
let rec checkpos_bound b n :=
match b with
| O ⇒ idtac
| S ?b´ ⇒
match n with
| xH ⇒ idtac
| xI ?n´ ⇒ checkpos_bound b´ n´
| xO ?n´ ⇒ checkpos_bound b´ n´
| _ ⇒ fail 1
end
end in
checkpos_bound 16%nat n.
Ltac const_Z n :=
match n with
| Z0 ⇒ idtac
| Zpos ?p ⇒ const_pos p
| Zneg ?p ⇒ const_pos p
| _ ⇒ fail 1
end.
Ltac is_const n :=
match n with
| O ⇒ idtac
| S ?x ⇒ const_nat x
| Z0 ⇒ idtac
| Zpos ?x ⇒ const_pos x
| Zneg ?x ⇒ const_pos x
| xH ⇒ idtac
| xI ?x ⇒ const_pos x
| xO ?x ⇒ const_pos x
| _ ⇒ fail 1
end.
Ltac z_of_nat_const n :=
is_const n;
let z := fresh "z" in
let Hz := fresh "Heq" z in
remember (Z.of_nat n) as z eqn: Hz;
simpl in Hz; rewrite Hz; clear Hz.
Ltac z_to_nat_const z :=
is_const z;
let n := fresh "n" in
let Hn := fresh "Heq" n in
remember (Z.to_nat z) as n eqn: Hn;
unfold Z.to_nat in Hn; unfold Pos.to_nat in Hn;
simpl in Hn; rewrite Hn; clear Hn.
Ltac z_expr_const e :=
let x := fresh "x" in
let Hx := fresh "Heq" x in
remember e as x eqn: Hx;
compute in Hx; rewrite Hx; clear x Hx.
Ltac print_goal :=
match goal with [|- ?g] ⇒ idtac g end.
SearchAbout (_ ^ (_ + _)).
Ltac calc_term e :=
match e with
| (?n + ?m)%Z ⇒
first [is_const n; first [is_const m; z_expr_const (n + m)%Z | idtac ] |
first [is_const m; idtac; rewrite (Z.add_comm n m) | idtac ]; calc_term n; repeat rewrite Z.add_assoc]
| (?n × ?m)%Z ⇒
first [is_const n; first [is_const m; z_expr_const (n × m)%Z | idtac ] |
first [is_const m; rewrite (Z.mul_comm n m) | idtac ]; calc_term n; repeat rewrite Z.mul_assoc]
| (?n - ?m)%Z ⇒
first [is_const n; first [is_const m; z_expr_const (n - m)%Z | idtac ] |
first [is_const m; first [rewrite (Z_minus_comm n m) | rewrite (Z_minus_comm_minus n m)] | idtac ];
calc_term n; repeat rewrite Z.add_assoc; repeat rewrite Z_plus_assoc_minus]
| (?n ^ ?m)%Z ⇒
first [is_const n; first [is_const m; z_expr_const (n ^ m)%Z | idtac ] |
first [is_const m; calc_term n | idtac ]; calc_term m]
|_ ⇒ idtac
end.
Ltac calc_goal :=
repeat match goal with
| [|- context [(?n + ?m)%Z]] ⇒
is_const n; is_const m;
z_expr_const (n + m)
| [|- context [(?n × ?m)%Z]] ⇒
is_const n; is_const m;
z_expr_const (n × m)
| [|- context [(?n - ?m)%Z]] ⇒
is_const n; is_const m;
z_expr_const (n - m)
| [|- context [(?n ^ ?m)%Z]] ⇒
is_const n; is_const m;
z_expr_const (n ^ m)
| [|- context [(-(?n))%Z]] ⇒
is_const n;
z_expr_const (-(n))%Z
end.
Ltac pre_calc :=
repeat progress (
repeat rewrite Z.opp_add_distr;
repeat rewrite Z.mul_add_distr_l; repeat rewrite Z.mul_add_distr_r;
repeat rewrite Z.mul_sub_distr_l; repeat rewrite Z.mul_sub_distr_r;
repeat rewrite Z_plus_assoc_minus; repeat rewrite Z_minus_assoc_minus;
repeat rewrite Z_minus_assoc_plus; repeat rewrite Z.add_assoc;
repeat rewrite Z.mul_assoc).
Ltac calcing :=
match goal with
| [|- context [Z.of_nat ?n]] ⇒ z_of_nat_const n
| [|- context [Z.to_nat ?n]] ⇒ z_to_nat_const n
| [|- context [((?n + ?m) / ?p)%Z]] ⇒ is_const p;
let x := fresh "x" in
let Heqx := fresh "Heqx" in
first [
is_const n;
assert (p ≤ n) by omega;
remember (n - p) as x eqn: Heqx; ring_simplify in Heqx;
replace (n + m) with ((m + x) + 1 × p); [| try omega];
rewrite (Z.div_add (m + x) 1 p); [| try omega]
| is_const m;
assert (p ≤ m) by omega;
remember (m - p) as x eqn: Heqx; ring_simplify in Heqx;
replace (n + m) with ((n + x) + 1 × p); [calc_goal| try omega];
rewrite (Z.div_add (n + x) 1 p); [| try omega]
]; rewrite Heqx; clear x Heqx; try rewrite Z.add_0_r
| [|- context [(?n / ?m)%Z]] ⇒ first [is_const n; is_const m; z_expr_const (n / m)%Z |
let x := fresh "x" in
let Heqx := fresh "Heqx" in
remember n as x eqn: Heqx;
ring_simplify in Heqx;
rewrite Heqx;
clear x Heqx
]
| [|- context [(?n + ?m)%Z]] ⇒ calc_term (n + m)%Z; progress calc_goal
| [|- context [(?n - ?m)%Z]] ⇒ calc_term (n - m)%Z; progress calc_goal
| [|- context [(?a ^ ?n)%Z]] ⇒ calc_term (a ^ n)%Z; progress calc_goal
| [|- context [((?b × ?a) / ?a)%Z]] ⇒ rewrite Z_div_mult
| [|- context [((?a × ?b) / ?a)%Z]] ⇒ rewrite (Z.mul_comm a b); rewrite Z_div_mult
| [|- context [(?n × ?m)%Z]] ⇒ calc_term (n × m)%Z; progress calc_goal
| [|- context [(((?a + ?b) mod ?n + (?c mod ?n)) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_comm a b c n); [| try omega]
| [|- context [(((?a + ?b) mod ?n + ?c) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_comm_le a b c n); [| try omega | try omega]
| [|- context [((?a mod ?n) mod ?n)%Z]] ⇒ rewrite (Z.mod_mod a n); [| try omega]
| [|- ?x mod 2 ≠ 0] ⇒ let a := fresh "a" in
let b := fresh "b" in
let Heqa := fresh "Heqa" in
let Heqb := fresh "Heqb" in
remember (x - 1) as a eqn: Heqa;
remember (a / 2) as b eqn: Heqb;
replace x with (b × 2 + 1);
[rewrite Z_odd_mod; try omega |
rewrite Heqb; rewrite Z_mult_div;
[ rewrite Heqa; omega |
try omega |
ring_simplify in Heqa;
rewrite Heqa; try omega]
]
| [|- context [((?a + 0) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_0 a n); [| try omega]
| [|- context [((0 + ?a) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_0_l a n); [| try omega]
| [|- context [((?a + ?n) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_same a n); [| try omega]
| [|- context [((?n + ?a) mod ?n)%Z]] ⇒ rewrite (Z_add_mod_same_l a n); [| try omega]
| [|- context [((?n + ?m) mod ?p)%Z]] ⇒ let r := fresh "r" in
let x := fresh "x" in
let Heqr := fresh "Heqr" in
let Heqx := fresh "Heqx" in
first [
is_const n;
remember (n / p) as r eqn: Heqr; compute in Heqr;
remember (m + n - r × p) as x eqn: Heqx;
rewrite Heqr in Heqx; ring_simplify in Heqx;
replace (n + m) with (x + r × p) by omega;
rewrite Z.add_mod; [|try omega];
rewrite Z.mod_mul; [|try omega];
rewrite Z.add_0_r; rewrite Z.mod_mod; [| try omega]
| is_const m;
remember (m / p) as r eqn: Heqr; compute in Heqr;
remember (n + m - r × p) as x eqn: Heqx;
rewrite Heqr in Heqx; ring_simplify in Heqx;
replace (n + m) with (x + r × p) by omega;
rewrite Z.add_mod; [|try omega];
rewrite Z.mod_mul; [|try omega];
rewrite Z.add_0_r; rewrite Z.mod_mod; [| try omega]
]; rewrite Heqx; clear r x Heqr Heqx
| [|- context [((?a × ?b) mod ?b)%Z]] ⇒ rewrite Z.mod_mul; [| try omega]
| [|- context [((?b × ?a) mod ?b)%Z]] ⇒ rewrite Z.mul_comm; rewrite Z.mod_mul; [| try omega]
| [|- context [((?a × ?b) mod ?n)%Z]] ⇒ is_const n;
let Ha := fresh "Hassert" in
first [
is_const a;
assert (Ha: a mod n = 0) by reflexivity;
rewrite (Z_mult_mod a b n); [| try omega | try omega]
| is_const b;
assert (Ha: b mod n = 0) by reflexivity;
rewrite (Z.mul_comm a b);
rewrite (Z_mult_mod b a n); [| try omega | try omega]
]; clear Ha
| [|- context [(?n mod ?m)%Z]] ⇒ first [is_const n; is_const m; z_expr_const (n mod m)%Z |
let H := fresh "H" in
assert (H: 0 ≤ n < m) by omega;
rewrite (Z.mod_small n m) by omega;
clear H]
| _ ⇒ fail 1
end.
Ltac post_calc :=
try rewrite Z.add_0_r;
try rewrite Z.add_0_l;
try rewrite Z.mul_0_r;
try rewrite Z.mul_0_l;
try ring_simplify.
Ltac calc :=
pre_calc; repeat calcing; post_calc.
Ltac toZ_const :=
match goal with
| [|- context [Z.of_nat O]] ⇒ rewrite Z_OF_NAT_0
| [|- context [Z.of_nat 1]] ⇒ rewrite Z_OF_NAT_1
| [|- context [Z.of_nat 2]] ⇒ rewrite Z_OF_NAT_2
| [|- context [Z.of_nat 512]] ⇒ rewrite Z_OF_NAT_512
| [|- context [Z.of_nat (S ?a)]] ⇒
let n := fresh "n" in
let Hn := fresh "Hn" in
pose (n := (Z.of_nat (S a)));
assert (Hn: n = (Z.of_nat (S a))) by auto;
rewrite <- Hn;
unfold Z.of_nat in Hn;
simpl in Hn; rewrite Hn;
clear Hn; clear n
end.
Ltac toZ :=
match goal with
| [|- context [(_ ≤ _)%nat]] ⇒ rewrite Nat2Z.inj_le
| [|- context [(_ < _)%nat]] ⇒ rewrite Nat2Z.inj_lt
| [|- context [(_ ≥ _)%nat]] ⇒ rewrite Nat2Z.inj_ge
| [|- context [(_ > _)%nat]] ⇒ rewrite Nat2Z.inj_gt
| [|- context [(Z.abs_nat _)%nat]] ⇒ rewrite Nat2Z.inj_abs_nat
| [|- context [(min _ _)%nat]] ⇒ rewrite Nat2Z.inj_min
| [|- context [(max _ _)%nat]] ⇒ rewrite Nat2Z.inj_max
| [|- context [Z.of_nat (length _)]] ⇒ rewrite <- Zlength_correct
| [|- context [Z.of_nat (_ + _)%nat]] ⇒ rewrite Nat2Z.inj_add
| [|- context [Z.of_nat (_ - _)%nat]] ⇒ rewrite Nat2Z.inj_sub
| [|- context [Z.of_nat (_ × _)%nat]] ⇒ rewrite Nat2Z.inj_mul
| [|- context [Z.of_nat (Z.to_nat _)]] ⇒ rewrite Z2Nat.id
| [|- context [Z.of_nat (S (Z.to_nat _))]] ⇒
rewrite <- NPeano.Nat.add_1_r; rewrite Nat2Z.inj_add; rewrite Z2Nat.id; [rewrite Z_OF_NAT_1|]
| [|- context [Z.of_nat O]] ⇒ toZ_const
| [|- context [Z.of_nat (S _)]] ⇒ toZ_const
| [|- context [(Z.succ _ - 1)%Z]] ⇒ rewrite Z_succ_pred
| _ ⇒ fail 1 "cannot find any nat to Z"
end.
Ltac toNat :=
match goal with
| [|- context [(_ ≤ _)%Z]] ⇒ rewrite Z2Nat.inj_le by omega
| [|- context [(_ < _)%Z]] ⇒ rewrite Z2Nat.inj_lt by omega
| [|- context [Z.to_nat (_ + _)%Z]] ⇒ rewrite Z2Nat.inj_add by omega
| [|- context [Z.to_nat (_ - _)%Z]] ⇒ rewrite Z2Nat.inj_sub by omega
| [|- context [Z.to_nat (_ × _)%Z]] ⇒ rewrite Z2Nat.inj_mul by omega
| [|- context [Z.of_nat (Z.to_nat _)]] ⇒ rewrite Z2Nat.id by omega
| [|- context [Z.to_nat (Z.succ _)]] ⇒ rewrite Z2Nat.inj_succ by omega
| [|- context [Z.to_nat (1 + _)%Z]] ⇒ rewrite Z2Nat.inj_succ by omega
| [|- context [Z.to_nat (_ + 1)%Z]] ⇒ rewrite Z.add_1_r; rewrite Z2Nat.inj_add by omega
| [|- context [Z.to_nat (Z.pred _)]] ⇒ rewrite Z2Nat.inj_pred by omega
| [|- context [Z.to_nat (_ - 1)%Z]] ⇒ rewrite Z2Nat.inj_pred by omega
| [|- context [(min _ _)%nat]] ⇒ rewrite Z2Nat.inj_min by omega
| [|- context [(max _ _)%nat]] ⇒ rewrite Z2Nat.inj_max by omega
| [|- context [Z.to_nat 0%Z]] ⇒ rewrite Z2Nat.inj_0 by omega
| [|- context [Z.to_nat 1%Z]] ⇒ rewrite Z_TO_NAT_1 by omega
| [|- context [Z.to_nat (Z.neg _)]] ⇒ rewrite Z2Nat.inj_neg by omega
| [|- context [Z.to_nat (Z.pos ?x)]] ⇒
let z := fresh "z" in
let Hz := fresh "Hz" in
pose (z := Z.to_nat (Z.pos x));
assert (Hz: z = (Z.to_nat (Z.pos x))) by auto;
rewrite <- Hz; unfold Z.to_nat in Hz;
unfold Pos.to_nat in Hz; simpl in Hz;
rewrite Hz; clear Hz; clear z
| [|- context [(_ + 1)%nat]] ⇒ rewrite NPeano.Nat.add_1_r
| [|- context [(1 + _)%nat]] ⇒ rewrite NPeano.Nat.add_1_l
| _ ⇒ fail 1 "cannot find any Z to nat"
end.
Ltac case_if :=
match goal with
| [|- context [if ?cond then _ else _]] ⇒
let Hcase := fresh "Hcase" in destruct cond eqn: Hcase
| _ ⇒ fail 1 "cannot find 'if then else' in current goal"
end.
Ltac solve_list :=
match goal with
| [H: skipn ?n ?l = ?x :: ?tl |- context [firstn ?n ?l ++ ?x :: nil]] ⇒
rewrite <- (skipn_firstnp1 n l tl x H)
| [|- context [Zlength nil]] ⇒ rewrite Zlength_nil
| [|- context [firstn ?n ?l ++ ?x :: nil]] ⇒
rewrite <- (skipn_firstnp1 n l tl x)
| [|- context [Zlength (_ ++ _)]] ⇒ rewrite app_Zlength
| [|- context [length (_ ++ _)]] ⇒ rewrite app_length
| [|- context [Zlength (firstn _ _)]] ⇒ rewrite Zlength_correct
| [|- context [Zlength (skipn _ _)]] ⇒ rewrite Zlength_correct
| [|- context [length (firstn _ _)]] ⇒ rewrite firstn_length
| [|- context [length (skipn _ _)]] ⇒ rewrite length_skipn
| [|- context [skipn (length ?l) ?l]] ⇒ rewrite skipn_length
| [|- context [firstn (length ?l) ?l]] ⇒ rewrite firstn_length_eq
| [|- context [skipn 0 _]] ⇒ rewrite skip0_eq
| [|- context [(_ ++ _) ++ _]] ⇒ rewrite <- app_assoc
| [|- context [Zlength (_ :: _)]] ⇒ rewrite Zlength_cons
| [|- context [length (_ :: _)]] ⇒ rewrite <- length_cons
| [H1 : skipn ?n ?l = _ , H2 : (?n ≥ length ?l )%nat|- _ ] ⇒
generalize (skipn_ge l n H2);
let Hskip_nil := fresh "Hskip_nil" in
intros Hskip_nil; rewrite Hskip_nil in H1; try discriminate H1
| [|- context [firstn ?n (?h :: ?t)]] ⇒ rewrite firstn_dest
| [|- context [firstn _ nil]] ⇒ rewrite firstn_nil
| [|- context [(_ :: _) ++ _]] ⇒ rewrite <- app_comm_cons
| _ ⇒ fail 1 "cannot solve current goal"
end.
Ltac osubst :=
match goal with
| [ x := ?e |- _] ⇒ subst x
| _ ⇒ subst
end.
Ltac substx := repeat osubst.
Ltac iinv id :=
match goal with
| [H: ?f = ?r |- _] ⇒
match f with
| appcontext cxt [ ?g ?x ] ⇒
match x with
| id ⇒ functional inversion H; clear H
end
| _ ⇒
match r with
| appcontext cxt [ ?g ?x ] ⇒
match x with
| id ⇒ functional inversion H; clear H
end
end
end
end.
Require Import liblayers.compat.CompatGenSem.
Ltac preserves_invariants_direct low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H0: low_level_invariant _ _ |- _ ] ⇒
inversion H0; constructor; trivial
| [H0: high_level_invariant _ |- _ ] ⇒
inversion H0; constructor; simpl; intros; try congruence
| [H1: _ = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
simpl; try assumption
| _ ⇒ idtac
end
end.
Ltac preserves_invariants_subst low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H1: ?f = ret _ , H0: low_level_invariant _ _ |- _ ] ⇒
inversion H0; functional inversion H1; simpl in *; substx; try assumption; constructor; trivial
| [H1: _ = ret _ , H0: high_level_invariant _ |- _ ] ⇒
inversion H0; functional inversion H1; substx; try assumption; constructor; simpl; intros; try congruence
| [H1: _ = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
functional inversion H1; substx; simpl; try assumption
| _ ⇒ idtac
end
end.
Ltac preserves_invariants_nested low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H1: ?f = ret _ , H0: low_level_invariant _ _ |- _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
inversion H0; repeat (iinv d); simpl in *; substx; try assumption; constructor; trivial
end
| [H1: ?f = ret _ , H0: high_level_invariant _ |- _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
inversion H0; repeat (iinv d); simpl in *; substx; try assumption; constructor; simpl; intros; try congruence
end
| [H1: ?f = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
repeat (iinv d); simpl in *; substx; simpl; try assumption
end
| _ ⇒ idtac
end
end.
Ltac preserves_invariants_direct low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H0: low_level_invariant _ _ |- _ ] ⇒
inversion H0; constructor; trivial
| [H0: high_level_invariant _ |- _ ] ⇒
inversion H0; constructor; simpl; intros; try congruence
| [H1: _ = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
simpl; try assumption
| _ ⇒ idtac
end
end.
Ltac preserves_invariants_subst low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H1: ?f = ret _ , H0: low_level_invariant _ _ |- _ ] ⇒
inversion H0; functional inversion H1; simpl in *; substx; try assumption; constructor; trivial
| [H1: _ = ret _ , H0: high_level_invariant _ |- _ ] ⇒
inversion H0; functional inversion H1; substx; try assumption; constructor; simpl; intros; try congruence
| [H1: _ = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
functional inversion H1; substx; simpl; try assumption
| _ ⇒ idtac
end
end.
Ltac preserves_invariants_nested low_level_invariant high_level_invariant:=
constructor; simpl; intros;
match goal with
| [H: GenSem.semof _ _ _ _ _ |- _] ⇒
inv_generic_sem H;
match goal with
| [H1: ?f = ret _ , H0: low_level_invariant _ _ |- _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
inversion H0; repeat (iinv d); simpl in *; substx; try assumption; constructor; trivial
end
| [H1: ?f = ret _ , H0: high_level_invariant _ |- _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
inversion H0; repeat (iinv d); simpl in *; substx; try assumption; constructor; simpl; intros; try congruence
end
| [H1: ?f = ret _ , H0: _ ∧ _ |- _ ∧ _ ] ⇒
match f with
| appcontext cxt [ ?g ?d ] ⇒
repeat (iinv d); simpl in *; substx; simpl; try assumption
end
| _ ⇒ idtac
end
end.