Commit d6eb8351 authored by Xavier Denis's avatar Xavier Denis

Start proving type contexts

parent 29487f3a
Pipeline #45126 passed with stage
in 14 minutes and 33 seconds
......@@ -43,9 +43,10 @@ theories/typing/base.v
theories/typing/lft_contexts.v
theories/typing/uniq_cmra.v
theories/typing/type.v
# theories/typing/type_context.v
# theories/typing/cont_context.v
theories/typing/cont_context.v
theories/typing/type_context.v
theories/typing/maybe_uninit.v
# theories/typing/uninit.v
theories/typing/bool.v
theories/typing/int.v
theories/typing/mod_ty.v
......@@ -58,7 +59,7 @@ theories/typing/own.v
theories/typing/shr_bor.v
theories/typing/uniq_bor.v
# theories/typing/function.v
# theories/typing/programs.v
theories/typing/programs.v
# theories/typing/borrow.v
# theories/typing/cont.v
theories/typing/fixpoint.v
......
......@@ -249,6 +249,12 @@ Proof.
by rewrite Iff.
Qed.
Global Instance proph_obs_proper_eq :
Proper (pointwise_relation _ (=) ==> ()) proph_obs.
move=> ?? Iff. rewrite /proph_obs. do 4 f_equiv. apply forall_proper => ?.
by rewrite Iff.
Qed.
(** Manipulating Tokens *)
Lemma proph_tok_singleton ξ q : q:[ξ] q:+[[ξ]].
......
From lrust.typing Require Export type.
(* From lrust.typing Require Import programs. *)
From lrust.typing Require Import programs.
From lrust.util Require Import types.
(* From lrust.util Require Import types. *)
Set Default Proof Using "Type".
Implicit Type b: bool.
......@@ -13,32 +17,32 @@ Section bool.
Global Instance bool_send: Send bool_ty. Proof. done. Qed.
(*
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool_ty (λ post _, post -[b]).
Proof.
iIntros (E L tid) "_ _ _ $ $ _". iMod persistent_time_receipt_0 as "#H0".
iApply wp_value. rewrite tctx_interp_singleton tctx_hasty_val' //.
iExists 0%nat. iFrame "H0". by destruct b.
iIntros (E L tid post ?) "_ _ _ $ $ _ ?". iMod persistent_time_receipt_0 as "#H0".
iApply wp_value. iExists +[const b]. iFrame. rewrite tctx_interp_singleton tctx_hasty_val' //.
iExists 0%nat. iFrame "H0". eauto.
Qed.
Lemma type_bool (b : Datatypes.bool) E L C T x e :
Lemma type_bool {As} (b : Datatypes.bool) E L C (T : tctx As) x e pre:
Closed (x :b: []) e
(∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) -∗
typed_body E L C T (let: x := #b in e).
Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
Lemma type_if E L C T e1 e2 p:
p ◁ bool ∈ T →
typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
typed_body E L C T (if: p then e1 else e2).
( (v : val), typed_body E L C ((v bool_ty) +:: T) (subst' x v e) pre) -
typed_body E L C T (let: x := #b in e) (λ p, pre (b -:: p)).
Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done|done]. Qed.
Lemma type_if {As} E L C (T : tctx As) e1 e2 p pre1 pre2:
p bool_ty T
typed_body E L C T e1 pre1 - typed_body E L C T e2 pre2 -
typed_body E L C T (if: p then e1 else e2) (λ a, pre1 a /\ pre2 a).
Proof.
iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #TIME #HE Htl HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
iIntros (Hp) "He1 He2". iIntros (tid V) "#LFT #TIME #HE Htl HL HC HT Hv".
iDestruct (big_sepHLZip'_elem_of _ _ _ _ Hp with "HT") as (?) "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros (depth [[| |[|[]|]]|]) "_ _ H1"; try done; wp_case.
- iApply ("He2" with "LFT TIME HE Htl HL HC HT").
iIntros (depth [[| |[|[]|]]|]) "_ _ H1"; try (iDestruct "H1" as ([|]) "[_ %]"; done); wp_case.
- iApply ("He2" with "LFT TIME HE Htl HL HC HT").
iApply (proph_obs_weaken with "Hv"). move => ? [? ?] //.
- iApply ("He1" with "LFT TIME HE Htl HL HC HT").
iApply (proph_obs_weaken with "Hv"); move => ? [? ?] //.
Qed.
*)
End bool.
From iris.proofmode Require Import tactics.
From lrust.lang Require Import notation.
From lrust.typing Require Import type lft_contexts type_context.
From lrust.util Require Import types.
Set Default Proof Using "Type".
Section cont_context_def.
......@@ -9,14 +11,14 @@ Section cont_context_def.
Definition cont_postcondition : iProp Σ := True%I.
Record cctx_elt : Type :=
CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
cctxe_n : nat; cctxe_T : vec val cctxe_n tctx }.
CCtx_iscont { cctxe_k : val; cctxe_L : llctx; cctxe_As : Types; (* temp hack*)
cctxe_n : nat; cctxe_T : vec val cctxe_n tctx cctxe_As }.
End cont_context_def.
Add Printing Constructor cctx_elt.
Notation cctx := (list cctx_elt).
Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ _ T)
(at level 70, format "k ◁cont( L , T )").
Section cont_context.
......@@ -24,12 +26,12 @@ Section cont_context.
Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
let '(k cont(L, T)) := x in
( args, na_own tid - llctx_interp L 1 - tctx_interp tid (T args) -
( args V, na_own tid - llctx_interp L 1 - tctx_interp tid (T args) V -
WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
( (x : cctx_elt), x C - cctx_elt_interp tid x)%I.
Global Instance cctx_interp_permut tid:
(* Global Instance cctx_interp_permut tid:
Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
Proof. solve_proper. Qed.
......@@ -38,7 +40,7 @@ Section cont_context.
Proof.
iSplit.
- iIntros "H". iSplit; [|iIntros (??)]; iApply "H"; rewrite elem_of_cons; auto.
- iIntros "H". iIntros (? Hin). revert Hin. rewrite elem_of_cons=>-[->|?].
- iIntros "H". iIntros (? Hin). revert Hin. rewrite elem_of_cons. intros [-> |?].
+ by iDestruct "H" as "[H _]".
+ iDestruct "H" as "[_ H]". by iApply "H".
Qed.
......@@ -55,17 +57,17 @@ Section cont_context.
Lemma cctx_interp_singleton tid x :
cctx_interp tid [x] ≡ cctx_elt_interp tid x.
Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed.
Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed. *)
Lemma fupd_cctx_interp tid C :
(* Lemma fupd_cctx_interp tid C :
(|={⊤}=> cctx_interp tid C) -∗ cctx_interp tid C.
Proof.
rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
rewrite /cctx_interp. iIntros "H". iIntros ([k L n As T]) "%".
iIntros (args) "HL HT". iMod "H".
by iApply ("H" $! (k ◁cont(L, T)) with "[%] HL HT").
Qed.
Qed. *)
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
(* Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
∀ tid, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid C1 -∗ cctx_interp tid C2.
Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
......@@ -80,9 +82,9 @@ Section cont_context.
Proof.
rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid) "_ #HE H * %".
iApply ("H" with "[%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons E k L n (T1 T2 : vec val n tctx) C1 C2 :
Qed. *)
(*
Lemma cctx_incl_cons {As} E k L n (T1 T2 : vec val n → tctx As) C1 C2 :
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
Proof.
......@@ -111,7 +113,7 @@ Section cont_context.
rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
[iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
Qed.
Qed. *)
End cont_context.
Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
(* Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing. *)
From lrust.lang Require Import proofmode memcpy.
From lrust.typing Require Export type lft_contexts type_context cont_context.
From lrust.util Require Import types.
Set Default Proof Using "Type".
Section typing.
......@@ -7,28 +9,29 @@ Section typing.
(** Function Body *)
(* This is an iProp because it is also used by the function type. *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
( tid, lft_ctx - time_ctx - elctx_interp E - na_own tid - llctx_interp L 1 -
cctx_interp tid C - tctx_interp tid T -
Definition typed_body {As} (E : elctx) (L : llctx) (C : cctx) (T : tctx As)
(e : expr) (pre : xprod As Prop): iProp Σ :=
( tid V, lft_ctx - time_ctx - elctx_interp E - na_own tid - llctx_interp L 1 -
cctx_interp tid C - tctx_interp tid T V -
π, pre (tctx_values π V) -
WP e {{ _, cont_postcondition }})%I.
Global Arguments typed_body _ _ _ _ _%E.
Global Arguments typed_body _ _ _ _ _ _%E.
Global Instance typed_body_llctx_permut E :
(* Global Instance typed_body_llctx_permut E :
Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
Proof.
intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
by setoid_rewrite HL.
Qed.
Qed. *)
Global Instance typed_body_elctx_permut :
(* Global Instance typed_body_elctx_permut :
Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
Proof.
intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body.
by setoid_rewrite HE.
Qed.
Qed. *)
Global Instance typed_body_mono E L:
(* Global Instance typed_body_mono E L:
Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
(typed_body E L).
Proof.
......@@ -37,23 +40,24 @@ Section typing.
iMod (HT with "LFT HE HL HT") as "(HL & HT)".
iApply ("H" with "LFT TIME HE Htl HL [HC] HT").
by iApply (HC with "LFT HE HC").
Qed.
Qed. *)
Global Instance typed_body_mono_flip E L:
(* Global Instance typed_body_mono_flip E L:
Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip (⊢))
(typed_body E L).
Proof. intros ?????????. by eapply typed_body_mono. Qed.
Proof. intros ?????????. by eapply typed_body_mono. Qed. *)
(** Instruction *)
Definition typed_instruction (E : elctx) (L : llctx)
(T1 : tctx) (e : expr) (T2 : val tctx) : iProp Σ :=
( tid, lft_ctx - time_ctx - elctx_interp E - na_own tid -
llctx_interp L 1 - tctx_interp tid T1 -
WP e {{ v, na_own tid
llctx_interp L 1 tctx_interp tid (T2 v) }})%I.
Global Arguments typed_instruction _ _ _ _%E _.
(** Writing and Reading **)
Definition typed_instruction {As Bs} (E : elctx) (L : llctx)
(T1 : tctx As) (e : expr) (T2 : val tctx Bs) (pre : (xprod Bs Prop) xprod As Prop): iProp Σ :=
( tid post V1, lft_ctx - time_ctx - elctx_interp E - na_own tid -
llctx_interp L 1 - tctx_interp tid T1 V1 -
⟨π, pre (post π) (tctx_values π V1) -
WP e {{ 𝔳, V', (na_own tid
llctx_interp L 1 tctx_interp tid (T2 𝔳) V' π, post π (tctx_values π V') )}})%I.
Global Arguments typed_instruction _ _ _ _ _ _ _%E _.
(* * Writing and Reading *
Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
(□ ∀ v depth tid F qL, ⌜↑lftN ∪ ↑lrustN ⊆ F⌝ →
lft_ctx -∗ elctx_interp E -∗ llctx_interp L qL -∗ ty1.(ty_own) depth tid [v] ={F}=∗
......@@ -88,30 +92,30 @@ Section typing.
Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
Persistent (typed_read E L ty1 ty ty2).
Proof. rewrite typed_read_eq. apply _. Qed.
Proof. rewrite typed_read_eq. apply _. Qed. *)
End typing.
Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
(e : expr) (ty : type) : iProp Σ :=
typed_instruction E L T e (λ v, [v ty]).
Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
Definition typed_instruction_ty {As A} `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx As)
(e : expr) (ty : type A) pre : iProp Σ :=
typed_instruction E L T e (λ 𝔳, +[𝔳 ty]) pre.
Arguments typed_instruction_ty {_ _} {_ _} _ _ _ _%E _%T _.
Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
E L, typed_instruction_ty E L [] (of_val v) ty.
Arguments typed_val _ _ _%V _%T.
Definition typed_val {A} `{!typeG Σ} (v : val) (ty : type A) pre : Prop :=
E L, typed_instruction_ty E L +[] (of_val v) ty pre.
Arguments typed_val {_} {_ _} _%V _%T.
Section typing_rules.
Context `{!typeG Σ}.
(* This lemma is helpful when switching from proving unsafe code in Iris
back to proving it in the type system. *)
Lemma type_type E L C T e :
typed_body E L C T e - typed_body E L C T e.
Lemma type_type {As} E L C (T : tctx As) e p:
typed_body E L C T e p - typed_body E L C T e p.
Proof. done. Qed.
(* TODO: Proof a version of this that substitutes into a compatible context...
if we really want to do that. *)
Lemma type_equivalize_lft E L C T κ1 κ2 e :
(* Lemma type_equivalize_lft E L C T κ1 κ2 e :
(⊢ typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e) →
⊢ typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
Proof.
......@@ -119,21 +123,48 @@ Section typing_rules.
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
iApply (He with "LFT TIME [Hκ1 Hκ2 HE] Htl HL HC HT").
rewrite /elctx_interp /=. by iFrame.
Qed.
Qed. *)
Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
Definition let_trans {A1 A2 O} (p : (xprod A2 Prop) xprod A1 Prop) (x : xprod (A2 ^++ O) Prop): xprod (A1 ^++ O) Prop :=
λ a1o, let '(a1, o) := xprod_split a1o in
p (λ a2, x (a2 -++ o)) a1.
Lemma type_let' {A B D} E L (T1 : tctx A) (T2 : val tctx B) (T : tctx D) C xb e e' trans pre:
Closed (xb :b: []) e'
typed_instruction E L T1 e T2 -
( v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -
typed_body E L C (T1 ++ T) (let: xb := e in e').
typed_instruction E L T1 e T2 trans -
( v : val, typed_body E L C (T2 v h++ T) (subst' xb v e') pre) -
typed_body E L C (T1 h++ T) (let: xb := e in e') (let_trans trans pre).
Proof.
iIntros (Hc) "He He'". iIntros (tid) "#LFT #TIME #HE Htl HL HC HT".
iIntros (Hc) "He He'". iIntros (tid V) "#LFT #TIME #HE Htl HL HC HT #Hp".
destruct (hlist_app_split V) as (V1 & V2 & ->).
rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
{ iApply ("He" with "LFT TIME HE Htl HL HT1"). }
iIntros (v) "/= (Htl & HL & HT2)". wp_let.
iApply ("He'" with "LFT TIME HE Htl HL HC [HT2 HT]").
{
rewrite /let_trans.
setoid_rewrite (tctx_values_split V1 V2).
iApply ("He" with "LFT TIME HE Htl HL HT1 Hp").
}
iIntros (v). iIntros "Hx". iDestruct "Hx" as (x) "(Htl & HL & HT2 & ?)". wp_let.
iApply ("He'" $! v tid (x h++ V2) with "LFT TIME HE Htl HL HC [HT2 HT]").
rewrite tctx_interp_app. by iFrame.
iClear "Hp".
rewrite (proph_obs_proper); [ | intro; rewrite tctx_values_merge]; done.
Qed.
(*
Lemma incl_values_compat {A B C } E L (T : tctx A) (T1 : tctx B) (T2 : tctx C) π f:
tctx_incl E L T (T1 h++ T2) f ->
f (tctx_values π T) = tctx_values π (T1 h++ T2).
Proof. *)
Lemma type_body_incl {A B} E L C (T : tctx A) (T' : tctx B) e pre f:
tctx_incl E L T T' f
typed_body E L C T' e pre -
typed_body E L C T e (f pre).
Proof.
iIntros (?) "Hb".
iIntros (tid V) "#LFT #TIME #HE Htl HL HC HT #Hp".
iMod (H with "LFT HE HL HT Hp") as (X) "(HL & Hp' & HT')".
by iApply ("Hb" with "LFT TIME HE Htl HL HC HT'").
Qed.
(* We do not make the [typed_instruction] hypothesis part of the
......@@ -141,17 +172,22 @@ Section typing_rules.
hypotheses. The is important, since proving [typed_instruction]
will instantiate [T1] and [T2], and hence we know what to search
for the following hypothesis. *)
Lemma type_let E L T T' T1 T2 C xb e e' :
(* λ d, let '(a, c) := xprod_split (f d) in trans (λ b, pre (xprod_merge b c)) a *)
Lemma type_let {A B Cs D} E L (T : tctx D) (T' : tctx Cs) (T1 : tctx A) (T2 : val tctx B) C xb e e' trans pre f g:
Closed (xb :b: []) e'
( typed_instruction E L T1 e T2)
tctx_extract_ctx E L T1 T T'
( v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) -
typed_body E L C T (let: xb := e in e').
( typed_instruction E L T1 e T2 trans)
tctx_extract_ctx E L T1 T T' f
f (let_trans trans pre) = g
( v : val, typed_body E L C (T2 v h++ T') (subst' xb v e') pre) -
typed_body E L C T (let: xb := e in e') g.
Proof.
unfold tctx_extract_ctx. iIntros (? He ->) "?". iApply type_let'; last done.
iApply He.
unfold tctx_extract_ctx. iIntros (? He ? <-) "?".
rewrite -(type_body_incl _ _ _ _ _ _ _ _ H0).
iApply type_let'; done.
Qed.
(*
Lemma type_seq E L T T' T1 T2 C e e' :
Closed [] e' →
(⊢ typed_instruction E L T1 e (λ _, T2)) →
......@@ -312,5 +348,5 @@ Section typing_rules.
Z.of_nat (ty.(ty_size)) = n →
typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
typed_body E L C T (p1 <-{n} !p2;; e).
Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
End typing_rules.
Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed. *)
End typing_rules.
This diff is collapsed.
......@@ -104,3 +104,21 @@ Next Obligation. move=> *. fun_ext=> ?. by apply absurd. Qed.
Global Instance void_iso `{Void A, Void B} : Iso absurd absurd.
Proof. split; fun_ext=> ?; by apply absurd. Qed.
(* Applicative Functors *)
Class Ap (M : Type Type) := ap : {A B}, M (A B) M A M B.
Infix "<*>" := ap (at level 61, left associativity).
(* Reader Monad *)
Global Instance reader_fmap R : FMap (() R) := λ _ _ f a r, f (a r).
Global Instance reader_ap R : Ap (() R) := λ _ _ f a r, f r (a r).
Global Instance reader_mret R : MRet (() R) := λ _ a _, a.
Global Instance reader_mbind R : MBind (() R) := λ _ _ f a r, f (a r) r.
Global Instance reader_mjoin R : MJoin (() R) := λ _ j r, j r r.
Lemma reader_fmap_ret R A B (f : A B) (a : A) : f <$> (@mret (() R) _ _ a) = @mret (() R) _ _ (f a).
by rewrite /mret /reader_mret /fmap /reader_fmap.
Qed.
\ No newline at end of file
......@@ -57,6 +57,12 @@ Fixpoint hnth {F B As} (y: F B) (xl: hlist F As) (i: nat) : F (tnth B As i) :=
match xl with +[] => y | x +:: xl' =>
match i with 0 => x | S j => hnth y xl' j end end.
Inductive elem_of_hlist {F A} : forall As, ElemOf (F A) (hlist F As) :=
| elem_of_hlist_here As (x : F A) (l : hlist F As) : x (x +:: l)
| elem_of_list_further {B} As (x : F A) (y : F B) (l : hlist F As) : x l -> x (y +:: l).
Global Existing Instance elem_of_hlist.
Notation hnthe := (hnth ).
Fixpoint hrepeat {F A} (x: F A) n : hlist F (trepeat A n) :=
......@@ -74,6 +80,14 @@ Lemma hnth_apply {F C B As} (fl: _ As) (y: F B) (x: C) i :
hnth y (fl +$ x) i = hnth (const y) fl i x.
Proof. move: i. elim fl; [done|]=> > IH [|i]; [done|]. by rewrite /= IH. Qed.
Lemma hlist_app_split {F As Bs} (H : hlist F (As ^++ Bs)) : H1 H2, H = H1 h++ H2.
Proof. induction As as [|?? IH].
- by exists +[], H.
- dependent destruction H.
destruct (IH H) as (H1 & H2 & ->).
by exists (f +:: H1), H2.
Qed.
Inductive HForall {F} (Φ: A, F A Prop) : {As}, hlist F As Prop :=
| HForall_nil: HForall Φ +[]
| HForall_cons {A As} (x: _ A) (xl: _ As) :
......@@ -113,7 +127,7 @@ Qed.
Lemma HForall2_nth {F G B As} (Φ: A, F A G A Prop) (x y: _ B) (xl yl: _ As) i :
Φ _ x y HForall2 Φ xl yl Φ _ (hnth x xl i) (hnth y yl i).
Proof.
move=> ? All. move: i. elim All=>/= [|> ???]; by [|case].
move=> ? All. move: i. elim All=>/= [|> ???]; by [|case].
Qed.
Global Instance HForall2_reflexive {F As} (R: A, F A F A Prop) :
......@@ -186,7 +200,7 @@ Proof.
[by case=> [[]?]|done|case=> [[? xl]yl]|case=> [? xl]].
- move: Eq. by move/equal_f/(.$ (xl, yl))=>/= ->.
- move: Eq'. move/equal_f/(.$ xl)=>/=. by case (psep xl)=> [??]=>/= ->.
Qed.
Qed.
Fixpoint prepeat {F A} (x: F A) n : plist F (trepeat A n) :=
match n with 0 => -[] | S m => x -:: prepeat x m end.
......@@ -331,6 +345,57 @@ Proof.
move=> ? All. move: i. elim All=>/= [|> ???]; by [|case].
Qed.
(* Products of types *)
Definition xprod_split_l {t1 t2} (x : xprod (t1 ^++ t2)) : xprod t1.
induction t1; simpl in *; intuition.
Defined.
Definition xprod_split_r {t1 t2} (x : xprod (t1 ^++ t2)) : xprod t2.
induction t1; simpl in *; intuition.
Defined.
Definition xprod_split {t1 t2} (x : xprod (t1 ^++ t2)) : xprod t1 * xprod t2.
induction t1; simpl in *; intuition.
Defined.
Definition xprod_singleton {A B} (f : A B) : xprod ^[A] xprod ^[B].
simpl; intuition.
Qed.
Definition xprod_bimap {s1 s2 t1 t2} (f : xprod s1 xprod s2) (g : xprod t1 xprod t2) : xprod (s1 ^++ t1) xprod (s2 ^++ t2).
intros; apply papp; eauto using xprod_split_l, xprod_split_r, papp.
Defined.
Lemma xprod_split_l_papp {T1 T2} (t1 : xprod T1) (t2 : xprod T2) : xprod_split_l (t1 -++ t2) = t1.
Proof.
induction T1.
- by destruct t1.
- destruct t1. simpl. f_equal. apply IHT1.
Qed.
(* TODO(xavier): use elim/IndPrinp: here *)
Lemma xprod_split_r_papp {T1 T2} (t1 : xprod T1) (t2 : xprod T2) : xprod_split_r (t1 -++ t2) = t2.
Proof.
induction T1 as [|???IH]; destruct t1; simpl.
- done.
- by simpl; rewrite IH.
Qed.
Lemma bimap_distr {T1 T2 S1 S2} f g t1 t2 :
@xprod_bimap T1 T2 S1 S2 f g (t1 -++ t2) = f t1 -++ g t2.
Proof.
rewrite /xprod_bimap xprod_split_l_papp !xprod_split_r_papp //.
Qed.
Definition xprod_second {s1 t1 t2} (g : xprod t1 xprod t2) : xprod (s1 ^++ t1) xprod (s1 ^++ t2).
eauto using xprod_bimap.
Qed.
Definition xprod_first {s1 s2 t1} (g : xprod s1 xprod s2) : xprod (s1 ^++ t1) xprod (s2 ^++ t1).
eauto using xprod_bimap.
Qed.
(** * Sum *)
Inductive xsum As : Type := xinj (i: nat) : tnthe As i xsum As.
......@@ -417,6 +482,17 @@ Fixpoint big_sepHLZip {F G H As Bs} (Φ: ∀A B, F A → G B → H A B → PROP)
| x +:: xl', y +:: yl', z -:: zl' => Φ _ _ x y z big_sepHLZip Φ xl' yl' zl'
| _, _, _ => False end%I.
Fixpoint big_sepHLZip' {F G As} (Φ: A, F A G A PROP)
(xl: hlist F As) (yl: hlist G As) : PROP.
refine (
(match xl in hlist _ a, yl in hlist _ b return a = b PROP with
| x +:: xs, y +:: yl => λ eq , Φ _ x (_ y) _
| _, _ => λ eq , True%I