Module SemanticsValues

Set Implicit Arguments.
Require Import MyTactics.
Require Import Coercions.
Require Import Store.
Require Import RawPrograms.
Require Import Layers.
Require Import Programs.
Require Import ValueLists.
Require Import PathSemantics.
Require Import Erasure.
Require Import RevelationDefinition.


Notation VCoApps c vs :=
  (vmap (VCoApp c) vs).

Notation VTyAbss vs :=
  (vmap VTyAbs vs).

Inductive redv : value -> value -> Prop :=
| RedCoId:
    forall v,
    redv
      (VCoApp CoId v)
      v
| RedCoSeq:
    forall c1 c2 v,
    redv
      (VCoApp (CoSeq c1 c2) v)
      (VCoApp c2 (VCoApp c1 v))
| RedCoForallIntro:
    forall v,
    redv
      (VCoApp CoForallIntro v)
      (VTyAbs v)
| RedCoForallElim:
    forall v,
    redv
      (VCoApp CoForallElim (VTyAbs v))
      v
| RedCoExistsIntro:
    forall v,
    redv
      (VCoApp CoExistsIntro v)
      (VPack v)
| RedCoExistsLeftIntro:
    forall t,
    redv
      (VCoApp CoExistsLeftIntro (VTyAbs (VAbs t)))
      (VAbs (TLetUnpack (VVar 0) (lift_term 1 t)))
| RedCoExistsElim:
    forall v,
    redv
      (VCoApp CoExistsElim (VPack v))
      v
| RedCoArrow:
    forall t c1 c2,
    redv
      (VCoApp (CoArrow c1 c2) (VAbs t))
      (VAbs (TCoApp c2 (subst_term (VCoApp c1 (VVar 0)) 1 (lift_term 0 t))))
| RedCoPair:
    forall layer1 layer2 v1 v2 c1 c2,
    redv
      (VCoApp (CoPair layer1 layer2 c1 c2) (VPair layer1 layer2 v1 v2))
      (VPair layer1 layer2 (VCoApp c1 v1) (VCoApp c2 v2))
| RedCoForall:
    forall c v,
    redv
      (VCoApp (CoForall c) (VTyAbs v))
      (VTyAbs (VCoApp c v))
| RedCoExists:
    forall c v,
    redv
      (VCoApp (CoExists c) (VPack v))
      (VPack (VCoApp c v))
| RedCoBang:
    forall c v,
    redv
      (VCoApp (CoBang c) (VBang v))
      (VBang (VCoApp c v))
| RedCoRegionCap:
    forall c vs,
    redv
      (VCoApp (CoRegionCap c) (VRegionCap vs))
      (VRegionCap (VCoApps c vs))
| RedCoRegionCapPunched:
    forall c vs,
    redv
      (VCoApp (CoRegionCapPunched c) (VRegionCapPunched vs))
      (VRegionCapPunched (VCoApps c vs))
| RedCoRef:
    forall c l v,
    redv
      (VCoApp (CoRef c) (VLoc l v))
      (VLoc l (VCoApp c v))
| RedCoDereliction:
    forall v,
    redv
      (VCoApp CoDereliction (VBang v)) v
| RedCoBangIdempotent:
    forall v,
    redv
      (VCoApp CoBangIdempotent (VBang v)) (VBang (VBang v))
| RedCoPairBang:
    forall layer1 layer2 v1 v2,
    redv
      (VCoApp CoPairBang (VPair layer1 layer2 (VBang v1) (VBang v2)))
      (VBang (VPair layer1 layer2 v1 v2))
| RedCoBangPair:
    forall layer1 layer2 v1 v2,
    redv
      (VCoApp CoBangPair (VBang (VPair layer1 layer2 v1 v2)))
      (VBang (VPair layer1 layer2 (VBang v1) (VBang v2)))
| RedCoUnitBang:
    forall layer,
    redv
      (VCoApp CoUnitBang (VUnit layer))
      (VBang (VUnit layer))
| RedCoAtBang:
    forall v,
    redv
      (VCoApp CoAtBang (VInhabitant v))
      (VBang (VInhabitant v))
| RedCoDistrib:
    forall t,
    redv
      (VCoApp CoDistrib (VTyAbs (VAbs t)))
      (VAbs (TTyAbs (subst_term (VCoApp CoForallElim (VVar 0)) 1 (lift_term 0 t))))
| RedCoSingletonToGroup:
    forall vs,
    redv
      (VCoApp CoSingletonToGroup (VRegionCap vs))
      (VRegionCap vs)
| RedCoForallPair:
    forall layer1 layer2 v1 v2,
    redv
      (VCoApp CoForallPair (VTyAbs (VPair layer1 layer2 v1 v2)))
      (VPair layer1 layer2 (VTyAbs v1) (VTyAbs v2))
| RedCoForallBang:
    forall v,
    redv
      (VCoApp CoForallBang (VTyAbs (VBang v)))
      (VBang (VTyAbs v))
| RedCoForallRef:
    forall l v,
    redv
      (VCoApp CoForallRef (VTyAbs (VLoc l v)))
      (VLoc l (VTyAbs v))
| RedCoForallRegionCap:
    forall vs,
    redv
      (VCoApp CoForallRegionCap (VTyAbs (VRegionCap vs)))
      (VRegionCap (VTyAbss vs))
| RedCoForallRegionCapPunched:
    forall vs,
    redv
      (VCoApp CoForallRegionCapPunched (VTyAbs (VRegionCapPunched vs)))
      (VRegionCapPunched (VTyAbss vs))
| RedCoSingletonRegionCapExists:
    forall v,
    redv
      (VCoApp CoSingletonRegionCapExists (VRegionCap (VCons (VPack v) VNil)))
      (VPack (VRegionCap (VCons v VNil)))
| RedCoPairExistsLeft:
    forall layer1 layer2 v1 v2,
    redv
      (VCoApp CoPairExistsLeft (VPair layer1 layer2 (VPack v1) v2))
      (VPack (VPair layer1 layer2 v1 v2))
| RedCoPairExistsRight:
    forall layer1 layer2 v1 v2,
    redv
      (VCoApp CoPairExistsRight (VPair layer1 layer2 v1 (VPack v2)))
      (VPack (VPair layer1 layer2 v1 v2))
| RedCoBangExists:
    forall v,
    redv
      (VCoApp CoBangExists (VBang (VPack v)))
      (VPack (VBang v))
| RedCoRefExists:
    forall l v,
    redv
      (VCoApp CoRefExists (VLoc l (VPack v)))
      (VPack (VLoc l v))
| RedCoDefocus:
    forall pi v1 v2 v'1 v''1,
    select pi v1 (VInhabitant v''1) ->
    plug pi v1 v2 v'1 ->
    redv
      (VCoApp (CoDefocus pi) (VMixPair v1 (VRegionCap (VCons v2 VNil))))
      v'1
| RedCoDefocusGroup:
    forall v vs,
    redv
      (VCoApp CoDefocusGroup (VLogPair (VRegionCap (VCons v VNil)) (VRegionCapPunched vs)))
      (VRegionCap (VCons v vs))
| RedCoStarCommutative:
    forall layer1 layer2 v1 v2,
    (layer1 = Logical \/ layer2 = Logical) ->
    redv
      (VCoApp CoStarCommutative (VPair layer1 layer2 v1 v2))
      (VPair layer2 layer1 v2 v1)
| RedCoStarAssociative:
    forall layer1 layer2 layer3 v1 v2 v3,
    layer1 = Logical \/ layer2 = Logical \/ layer3 = Logical ->
    redv
      (VCoApp CoStarAssociative (VPair (layer_conj layer1 layer2) layer3 (VPair layer1 layer2 v1 v2) v3))
      (VPair layer1 (layer_conj layer2 layer3) v1 (VPair layer2 layer3 v2 v3))
| RedCoStarRef:
    forall l v1 v2,
    redv
      (VCoApp CoStarRef (VMixPair (VLoc l v1) v2))
      (VLoc l (VMixPair v1 v2))
| RedCoRefStar:
    forall l v1 v2,
    redv
      (VCoApp CoRefStar (VLoc l (VMixPair v1 v2)))
      (VMixPair (VLoc l v1) v2)
| RedCoStarSingleton:
    forall v1 v2,
    redv
      (VCoApp CoStarSingleton (VLogPair (VRegionCap (VCons v1 VNil)) v2))
      (VRegionCap (VCons (VMixPair v1 v2) VNil))
| RedCoSingletonStar:
    forall v1 v2,
    redv
      (VCoApp CoSingletonStar (VRegionCap (VCons (VMixPair v1 v2) VNil)))
      (VLogPair (VRegionCap (VCons v1 VNil)) v2)
| RedCoTensorExchangeVAbs:
    forall n t,
    redv
      (VCoApp (CoTensorExchange n) (VAbs t))
      (VAbs (subst_term (VCoApp (CoComposExchangeUnder n) (VVar 0))
                        1
                        (TCoApp (CoComposExchangeUnder n) (lift_term 0 t))))
| RedCoTensorExchangeVPair:
    forall n layer1 layer2 v1 v2,
    redv
      (VCoApp (CoTensorExchange n) (VPair layer1 layer2 v1 v2))
      (VPair layer1 layer2 (VCoApp (CoTensorExchange n) v1) (VCoApp (CoTensorExchange n) v2))
| RedCoTensorExchangeVUnit:
    forall n layer,
    redv
      (VCoApp (CoTensorExchange n) (VUnit layer))
      (VUnit layer)
| RedCoTensorExchangeVTyAbs:
    forall n v,
    redv
      (VCoApp (CoTensorExchange n) (VTyAbs v))
      (VTyAbs (VCoApp (CoTensorExchange n) v))
| RedCoTensorExchangeVPack:
    forall n v,
    redv
      (VCoApp (CoTensorExchange n) (VPack v))
      (VPack (VCoApp (CoTensorExchange n) v))
| RedCoTensorExchangeVBang:
    forall n v,
    redv
      (VCoApp (CoTensorExchange n) (VBang v))
      (VBang (VCoApp (CoTensorExchange n) v))
| RedCoTensorExchangeVLoc:
    forall n l v,
    redv
      (VCoApp (CoTensorExchange n) (VLoc l v))
      (VLoc l (VCoApp (CoTensorExchange n) v))
| RedCoTensorExchangeVRegionCap:
    forall n vs,
    redv
      (VCoApp (CoTensorExchange n) (VRegionCap vs))
      (VRegionCap (VCoApps (CoTensorExchange n) vs))
| RedCoTensorExchangeVRegionCapPunched:
    forall n vs,
    redv
      (VCoApp (CoTensorExchange n) (VRegionCapPunched vs))
      (VRegionCapPunched (VCoApps (CoTensorExchange n) vs))
| RedCoTensorExchangeVInhabitant:
    forall n v,
    redv
      (VCoApp (CoTensorExchange n) (VInhabitant v))
      (VInhabitant v)
| RedCoMu:
    forall c v,
    ccontractive 0 c ->
    redv (VCoApp (CoMu c) v) (VCoApp (cunfold c) v)
| RedPairContextLeft:
    forall layer1 layer2 v1 v2 v,
    redv v1 v2 ->
    redv (VPair layer1 layer2 v1 v) (VPair layer1 layer2 v2 v)
| RedPairContextRight:
    forall layer1 layer2 v1 v2 v,
    redv v1 v2 ->
    redv (VPair layer1 layer2 v v1) (VPair layer1 layer2 v v2)
| RedVCoAppContext:
    forall c v1 v2,
    redv v1 v2 ->
    redv (VCoApp c v1) (VCoApp c v2)
| RedVTyAbsContext:
    forall v1 v2,
    redv v1 v2 ->
    redv
      (VTyAbs v1)
      (VTyAbs v2)
| RedVPackContext:
    forall v1 v2,
    redv v1 v2 ->
    redv
      (VPack v1)
      (VPack v2)
| RedVBangContext:
    forall v1 v2,
    redv v1 v2 ->
    redv (VBang v1) (VBang v2)
| RedVRegionCapContext:
    forall vs1 vs2,
    redvs vs1 vs2 ->
    redv (VRegionCap vs1) (VRegionCap vs2)
| RedVRegionCapPunchedContext:
    forall vs1 vs2,
    redvs vs1 vs2 ->
    redv (VRegionCapPunched vs1) (VRegionCapPunched vs2)
| RedVLocContext:
    forall l v1 v2,
    redv v1 v2 ->
    redv (VLoc l v1) (VLoc l v2)



with redvs : values -> values -> Prop :=
| RedvsHere:
    forall v1 v2 vs,
    redv v1 v2 ->
    redvs (VCons v1 vs) (VCons v2 vs)
| RedvsThere:
    forall v vs1 vs2,
    redvs vs1 vs2 ->
    redvs (VCons v vs1) (VCons v vs2).

Hint Constructors redv redvs.



Scheme redv_redvs_ind_v := Induction for redv Sort Prop
  with redv_redvs_ind_vs := Induction for redvs Sort Prop.

Combined Scheme redv_redvs_ind from redv_redvs_ind_v, redv_redvs_ind_vs.