Newer
Older
Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' :
length l = length k →
sublist_lookup i n l = Some l' → sublist_lookup i n k = Some k' →
length (g l') = length k' → zip_with f (g l') k' = g (zip_with f l' k') →
zip_with f (sublist_alter g i n l) k = sublist_alter g i n (zip_with f l k).
Proof.
unfold sublist_lookup, sublist_alter. intros Hlen; rewrite Hlen.
intros ?? Hl' Hk'. simplify_option_equality.
by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take,
!take_length_le, Hk' by (rewrite ?drop_length; auto with lia).
Qed.
Section zip.
Context {A B : Type}.
Implicit Types l : list A.
Implicit Types k : list B.
Lemma fst_zip l k : length l ≤ length k → fst <$> zip l k = l.
Proof. by apply fmap_zip_with_l. Qed.
Lemma snd_zip l k : length k ≤ length l → snd <$> zip l k = k.
Proof. by apply fmap_zip_with_r. Qed.
Lemma zip_fst_snd (lk : list (A * B)) : zip (fst <$> lk) (snd <$> lk) = lk.
Proof. by induction lk as [|[]]; f_equal'. Qed.
Lemma Forall2_fst P l1 l2 k1 k2 :
length l2 = length k2 → Forall2 P l1 k1 →
Forall2 (λ x y, P (x.1) (y.1)) (zip l1 l2) (zip k1 k2).
Proof.
rewrite <-Forall2_same_length. intros Hlk2 Hlk1. revert l2 k2 Hlk2.
induction Hlk1; intros ?? [|??????]; simpl; auto.
Qed.
Lemma Forall2_snd P l1 l2 k1 k2 :
length l1 = length k1 → Forall2 P l2 k2 →
Forall2 (λ x y, P (x.2) (y.2)) (zip l1 l2) (zip k1 k2).
Proof.
rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1.
induction Hlk2; intros ?? [|??????]; simpl; auto.
Qed.
Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
x ∈ zipped_map f l k ↔
∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
split.
* revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
{ by eexists [], k, z. }
destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(associative_L (++)).
* intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
intros l; right. by rewrite reverse_cons, <-!(associative_L (++)).
Qed.
Section zipped_list_ind.
Context {A} (P : list A → list A → Prop).
Robbert Krebbers
committed
Context (Pnil : ∀ l, P l []) (Pcons : ∀ l k x, P (x :: l) k → P l (x :: k)).
Fixpoint zipped_list_ind l k : P l k :=
match k with
| [] => Pnil _ | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
end.
End zipped_list_ind.
Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' :
zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
Proof.
revert l. induction k as [|x k IH]; simpl; [done |].
Robbert Krebbers
committed
inversion_clear 1. rewrite reverse_cons, <-(associative_L (++)). by apply IH.
Robbert Krebbers
committed
(** * Relection over lists *)
(** We define a simple data structure [rlist] to capture a syntactic
representation of lists consisting of constants, applications and the nil list.
Note that we represent [(x ::)] as [rapp (rnode [x])]. For now, we abstract
over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *)
Inductive rlist (A : Type) :=
rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
Robbert Krebbers
committed
Arguments rnil {_}.
Arguments rnode {_} _.
Arguments rapp {_} _ _.
Module rlist.
Fixpoint to_list {A} (t : rlist A) : list A :=
match t with
| rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
Robbert Krebbers
committed
end.
Notation env A := (list (list A)) (only parsing).
Definition eval {A} (E : env A) : rlist nat → list A :=
fix go t :=
match t with
| rnil => []
| rnode i => from_option [] (E !! i)
| rapp t1 t2 => go t1 ++ go t2
end.
Robbert Krebbers
committed
3092
3093
3094
3095
3096
3097
3098
3099
3100
3101
3102
3103
3104
3105
3106
3107
3108
3109
3110
3111
3112
3113
3114
3115
3116
3117
3118
3119
3120
3121
3122
3123
(** A simple quoting mechanism using type classes. [QuoteLookup E1 E2 x i]
means: starting in environment [E1], look up the index [i] corresponding to the
constant [x]. In case [x] has a corresponding index [i] in [E1], the original
environment is given back as [E2]. Otherwise, the environment [E2] is extended
with a binding [i] for [x]. *)
Section quote_lookup.
Context {A : Type}.
Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0.
Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0.
Global Instance quote_lookup_further E1 E2 x i y :
QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000.
End quote_lookup.
Section quote.
Context {A : Type}.
Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
Global Instance quote_nil: Quote E1 E1 [] rnil.
Global Instance quote_node E1 E2 l i:
QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000.
Global Instance quote_cons E1 E2 E3 x l i t :
QuoteLookup E1 E2 [x] i →
Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t).
Global Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2).
End quote.
Section eval.
Context {A} (E : env A).
Lemma eval_alt t : eval E t = to_list t ≫= from_option [] ∘ (E !!).
Proof.
induction t; csimpl.
Robbert Krebbers
committed
* by rewrite (right_id_L [] (++)).
* rewrite bind_app. by f_equal.
Qed.
Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
Lemma eval_Permutation t1 t2 :
to_list t1 ≡ₚ to_list t2 → eval E t1 ≡ₚ eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
Lemma eval_contains t1 t2 :
to_list t1 `contains` to_list t2 → eval E t1 `contains` eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
End eval.
End rlist.
Robbert Krebbers
committed
(** * Tactics *)
Ltac quote_Permutation :=
match goal with
| |- ?l1 ≡ₚ ?l2 =>
match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
change (rlist.eval E3 t1 ≡ₚ rlist.eval E3 t2)
end end
end.
Ltac solve_Permutation :=
quote_Permutation; apply rlist.eval_Permutation;
apply (bool_decide_unpack _); by vm_compute.
Robbert Krebbers
committed
Ltac quote_contains :=
match goal with
| |- ?l1 `contains` ?l2 =>
match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
change (rlist.eval E3 t1 `contains` rlist.eval E3 t2)
end end
end.
Ltac solve_contains :=
quote_contains; apply rlist.eval_contains;
apply (bool_decide_unpack _); by vm_compute.
Ltac decompose_elem_of_list := repeat
match goal with
| H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
| H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
| H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
end.
Ltac solve_length :=
simplify_equality';
repeat (rewrite fmap_length || rewrite app_length);
repeat match goal with
| H : @eq (list _) _ _ |- _ => apply (f_equal length) in H
| H : Forall2 _ _ _ |- _ => apply Forall2_length in H
| H : context[length (_ <$> _)] |- _ => rewrite fmap_length in H
end; done || congruence.
Ltac simplify_list_equality ::= repeat
| _ => progress simplify_equality'
| H : [?x] !! ?i = Some ?y |- _ =>
destruct i; [change (Some x = Some y) in H | discriminate]
| H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
| H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
Robbert Krebbers
committed
| H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
| H : [] = zip_with _ _ _ |- _ => symmetry in H
3188
3189
3190
3191
3192
3193
3194
3195
3196
3197
3198
3199
3200
3201
3202
3203
3204
3205
3206
3207
3208
3209
3210
3211
3212
3213
| |- context [(_ ++ _) ++ _] => rewrite <-(associative_L (++))
| H : context [(_ ++ _) ++ _] |- _ => rewrite <-(associative_L (++)) in H
| H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
| |- context [_ <$> (_ ++ _)] => rewrite fmap_app
| |- context [_ ++ []] => rewrite (right_id_L [] (++))
| H : context [_ ++ []] |- _ => rewrite (right_id_L [] (++)) in H
| |- context [take _ (_ <$> _)] => rewrite <-fmap_take
| H : context [take _ (_ <$> _)] |- _ => rewrite <-fmap_take in H
| |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
| H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
| H : _ ++ _ = _ ++ _ |- _ =>
repeat (rewrite <-app_comm_cons in H || rewrite <-(associative_L (++)) in H);
apply app_injective_1 in H; [destruct H|solve_length]
| H : _ ++ _ = _ ++ _ |- _ =>
repeat (rewrite app_comm_cons in H || rewrite (associative_L (++)) in H);
apply app_injective_2 in H; [destruct H|solve_length]
| |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
rewrite zip_with_app by solve_length
| |- context [take _ (_ ++ _)] => rewrite take_app_alt by solve_length
| |- context [drop _ (_ ++ _)] => rewrite drop_app_alt by solve_length
| H : context [zip_with _ (_ ++ _) (_ ++ _)] |- _ =>
rewrite zip_with_app in H by solve_length
| H : context [take _ (_ ++ _)] |- _ =>
rewrite take_app_alt in H by solve_length
| H : context [drop _ (_ ++ _)] |- _ =>
rewrite drop_app_alt in H by solve_length
Ltac decompose_Forall_hyps :=
repeat match goal with
| H : Forall _ [] |- _ => clear H
| H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
| H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
| H : Forall2 _ [] [] |- _ => clear H
| H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
| H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
| H : Forall2 _ [] ?k |- _ => apply Forall2_nil_inv_l in H
| H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H
| H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
Robbert Krebbers
committed
apply Forall2_cons_inv in H; destruct H
| H : Forall2 _ (_ :: _) ?k |- _ =>
let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in
apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->);
rename k_tl into k
| H : Forall2 _ ?l (_ :: _) |- _ =>
let l_hd := fresh l "_hd" in let l_tl := fresh l "_tl" in
apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->);
rename l_tl into l
| H : Forall2 _ (_ ++ _) ?k |- _ =>
let k1 := fresh k "_1" in let k2 := fresh k "_2" in
apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->)
| H : Forall2 _ ?l (_ ++ _) |- _ =>
let l1 := fresh l "_1" in let l2 := fresh l "_2" in
apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
| _ => progress simplify_equality'
| H : Forall3 _ _ (_ :: _) _ |- _ =>
apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
| H : Forall2 _ (_ :: _) ?k |- _ =>
apply Forall2_cons_inv_l in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ ?l (_ :: _) |- _ =>
apply Forall2_cons_inv_r in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
apply Forall2_app_inv in H; [destruct H|solve_length]
| H : Forall2 _ ?l (_ ++ _) |- _ =>
apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ (_ ++ _) ?k |- _ =>
apply Forall2_app_inv_l in H; destruct H as (?&?&?&?&?)
| H : Forall3 _ _ (_ ++ _) _ |- _ =>
apply Forall3_app_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
| H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
(* to avoid some stupid loops, not fool proof *)
unless (P x) by auto using Forall_app_2, Forall_nil_2;
Robbert Krebbers
committed
assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
| H : Forall2 ?P ?l ?k |- _ =>
| H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ =>
unless (P x y) by done; let E := fresh in
assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y));
Robbert Krebbers
committed
lazy beta in E
| H1 : l !! ?i = Some ?x |- _ =>
try (match goal with _ : k !! i = Some _ |- _ => fail 2 end);
destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
| H2 : k !! ?i = Some ?y |- _ =>
try (match goal with _ : l !! i = Some _ |- _ => fail 2 end);
destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
end
| H : Forall3 ?P ?l ?l' ?k |- _ =>
lazymatch goal with
| H1:l !! ?i = Some ?x, H2:l' !! ?i = Some ?y, H3:k !! ?i = Some ?z |- _ =>
unless (P x y z) by done; let E := fresh in
assert (P x y z) as E by (by apply (Forall3_lookup_lmr P l l' k i x y z));
lazy beta in E
| H1 : l !! _ = Some ?x |- _ =>
destruct (Forall3_lookup_l P _ _ _ _ _ H H1) as (?&?&?&?&?)
| H2 : l' !! _ = Some ?y |- _ =>
destruct (Forall3_lookup_m P _ _ _ _ _ H H2) as (?&?&?&?&?)
| H3 : k !! _ = Some ?z |- _ =>
destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?)
end
Ltac list_simplifier :=
simplify_equality';
repeat match goal with
| _ => progress decompose_Forall_hyps
| _ => progress simplify_list_equality
| H : _ <$> _ = _ :: _ |- _ =>
apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
| H : _ :: _ = _ <$> _ |- _ => symmetry in H
| H : _ <$> _ = _ ++ _ |- _ =>
apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
| H : _ ++ _ = _ <$> _ |- _ => symmetry in H
| H : zip_with _ _ _ = _ :: _ |- _ =>
apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
| H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
| H : zip_with _ _ _ = _ ++ _ |- _ =>
apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?&?)
| H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
end.
Ltac decompose_Forall := repeat
match goal with
| |- Forall _ _ => by apply Forall_true
| |- Forall _ [] => constructor
| |- Forall _ (_ :: _) => constructor
| |- Forall _ (_ ++ _) => apply Forall_app_2
| |- Forall _ (_ <$> _) => apply Forall_fmap
| |- Forall _ (_ ≫= _) => apply Forall_bind
| |- Forall2 _ _ _ => apply Forall2_Forall
| |- Forall2 _ [] [] => constructor
| |- Forall2 _ (_ :: _) (_ :: _) => constructor
| |- Forall2 _ (_ ++ _) (_ ++ _) => first
[ apply Forall2_app; [by decompose_Forall |]
| apply Forall2_app; [| by decompose_Forall]]
| |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
| |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
| _ => progress decompose_Forall_hyps
| H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
| H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
Robbert Krebbers
committed
apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
apply Forall2_lookup_2; [solve_length|];
intros ?????; progress decompose_Forall_hyps
end.
(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
[(++)]. *)
Ltac simplify_suffix_of := repeat
match goal with
Robbert Krebbers
committed
| H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H)
| H : suffix_of (_ :: _) [] |- _ => apply suffix_of_nil_inv in H
| H : suffix_of (_ ++ _) (_ ++ _) |- _ => apply suffix_of_app_inv in H
| H : suffix_of (_ :: _) (_ :: _) |- _ =>
destruct (suffix_of_cons_inv _ _ _ _ H); clear H
| H : suffix_of ?x ?x |- _ => clear H
| H : suffix_of ?x (_ :: ?x) |- _ => clear H
| H : suffix_of ?x (_ ++ ?x) |- _ => clear H
| _ => progress simplify_equality'
end.
(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
conclusions. This tactic either fails or proves the goal. *)
Robbert Krebbers
committed
Ltac solve_suffix_of := by intuition (repeat
match goal with
| _ => done
| _ => progress simplify_suffix_of
| |- suffix_of [] _ => apply suffix_of_nil
| |- suffix_of _ _ => reflexivity
| |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
| |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
| H : suffix_of _ _ → False |- _ => destruct H
Robbert Krebbers
committed
end).
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
unfold PropHolds; solve_suffix_of : typeclass_instances.