Commit ab930b45 authored by Robbert Krebbers's avatar Robbert Krebbers

Miscellaneous changes to the memory

* Remove generic path_typed instance for lists. For the zippers in the
  operational semantics, it goes the other way around.
* Remove constructor lemmas for values/memory_trees and use a generic tactic
  instead. This tactic uses the standard constructor tactic, but folds the
  type classes afterward.
parent 3ce93174
......@@ -761,6 +761,9 @@ Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le l k n : n length l take n (l ++ k) = take n l.
Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
Lemma take_plus_app l k n m :
length l = n take (n + m) (l ++ k) = l ++ take m k.
Proof. intros <-. induction l; f_equal'; auto. Qed.
Lemma take_app_ge l k n :
length l n take n (l ++ k) = l ++ take (n - length l) k.
Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
......@@ -2833,6 +2836,12 @@ Section zip_with.
Lemma zip_with_length_same_r P l k :
Forall2 P l k length (zip_with f l k) = length k.
Proof. induction 1; simpl; auto. Qed.
Lemma lookup_zip_with l k i :
zip_with f l k !! i = x l !! i; y k !! i; Some (f x y).
Proof.
revert k i. induction l; intros [|??] [|?]; f_equal'; auto.
by destruct (_ !! _).
Qed.
Lemma fmap_zip_with_l (g : C A) l k :
( x y, g (f x y) = x) length l length k g <$> zip_with f l k = l.
Proof. revert k. induction l; intros [|??] ??; f_equal'; auto with lia. Qed.
......
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