hlist.v 1.47 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export hlist.
2
From iris.base_logic Require Export base_logic.
3
Set Default Proof Using "Type".
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
Import uPred.

Fixpoint uPred_hexist {M As} : himpl As (uPred M)  uPred M :=
  match As return himpl As (uPred M)  uPred M with
  | tnil => id
  | tcons A As => λ Φ,  x, uPred_hexist (Φ x)
  end%I.
Fixpoint uPred_hforall {M As} : himpl As (uPred M)  uPred M :=
  match As return himpl As (uPred M)  uPred M with
  | tnil => id
  | tcons A As => λ Φ,  x, uPred_hforall (Φ x)
  end%I.

Section hlist.
Context {M : ucmraT}.

Lemma hexist_exist {As B} (f : himpl As B) (Φ : B  uPred M) :
  uPred_hexist (hcompose Φ f)   xs : hlist As, Φ (f xs).
Proof.
  apply (anti_symm _).
  - induction As as [|A As IH]; simpl.
    + by rewrite -(exist_intro hnil) .
    + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
      by rewrite -(exist_intro (hcons x xs)).
  - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
    by rewrite -(exist_intro x) IH.
30 31 32 33 34 35 36
Qed.

Lemma hforall_forall {As B} (f : himpl As B) (Φ : B  uPred M) :
  uPred_hforall (hcompose Φ f)   xs : hlist As, Φ (f xs).
Proof.
  apply (anti_symm _).
  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
    by rewrite (forall_elim x) IH.
38 39 40 41 42 43
  - induction As as [|A As IH]; simpl.
    + by rewrite (forall_elim hnil) .
    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
      by rewrite (forall_elim (hcons x xs)).
Qed.
End hlist.