Library zoo.language.physical_equality
Require Import zoo.prelude.
Require Export zoo.common.typeclasses.
Require Export zoo.common.math.
Require Export zoo.common.list.
Require Export zoo.language.syntax.
Require Import zoo.options.
Implicit Type i tag : nat.
Implicit Type n : Z.
Implicit Type l : location.
Implicit Type gen : generativity.
Implicit Type lit : literal.
Implicit Type v : val.
Implicit Type vs : list val.
Variant lowliteral :=
| LowlitInt n
| LowlitLoc l
| LowlitProph
| LowlitPoison.
Implicit Type llit : lowliteral.
#[global] Instance lowliteralｰeq_dec : EqDecision lowliteral :=
ltac:(solve_decision).
Definition literal۰to_low lit :=
match lit with
| LitBool b ⇒
LowlitInt (Nat.b2n b)
| LitInt n ⇒
LowlitInt n
| LitLoc l ⇒
LowlitLoc l
| LitProph _ ⇒
LowlitProph
| LitPoison ⇒
LowlitPoison
end.
#[global] Arguments literal۰to_low !_ / : simpl nomatch, assert.
#[global] Instance lowliteral۰nonsimilar : Nonsimilar lowliteral :=
λ llit1 llit2,
match llit1 with
| LowlitInt n1 ⇒
llit2 ≠ LowlitInt n1
| LowlitLoc l1 ⇒
llit2 ≠ LowlitLoc l1
| _ ⇒
True
end.
#[global] Instance lowliteralｰnonsimilarｰdec :
RelDecision (≉@{lowliteral}).
#[global] Instance lowliteralｰnonsimilarｰsymmetric :
Symmetric (≉@{lowliteral}).
Inductive lowval :=
| LowvalLit llit
| LowvalRecs
| LowvalBlock gen tag vs (lvs : list lowval).
Implicit Type lv : lowval.
Implicit Type lvs : list lowval.
Section lowval۰ind.
Variable P : lowval → Prop.
Variable HLit :
∀ llit,
P (LowvalLit llit).
Variable HRecs :
P LowvalRecs.
Variable HBlock :
∀ gen tag vs,
∀ lvs, Forall P lvs →
P (LowvalBlock gen tag vs lvs).
Fixpoint lowval۰ind lv :=
match lv with
| LowvalLit llit ⇒
HLit
llit
| LowvalRecs ⇒
HRecs
| LowvalBlock gen tag vs lvs ⇒
HBlock
gen tag vs
lvs (Forall_true P lvs lowval۰ind)
end.
End lowval۰ind.
Notation LowvalInt n := (
LowvalLit (LowlitInt n)
)(only parsing
).
Notation LowvalLoc l := (
LowvalLit (LowlitLoc l)
)(only parsing
).
Notation LowvalProph := (
LowvalLit LowlitProph
)(only parsing
).
Notation LowvalPoison := (
LowvalLit LowlitPoison
)(only parsing
).
#[global] Instance lowvalｰeq_dec : EqDecision lowval.
Fixpoint val۰to_low v :=
match v with
| ValLit llit ⇒
LowvalLit (literal۰to_low llit)
| ValRecs _ _ ⇒
LowvalRecs
| ValBlock _ tag [] ⇒
LowvalLit (LowlitInt tag)
| ValBlock gen tag vs ⇒
LowvalBlock gen tag vs (val۰to_low <$> vs)
end.
#[global] Arguments val۰to_low !_ / : simpl nomatch, assert.
#[global] Instance lowval۰nonsimilar : Nonsimilar lowval :=
λ lv1 lv2,
match lv1 with
| LowvalLit llit1 ⇒
match lv2 with
| LowvalLit llit2 ⇒
llit1 ≉ llit2
| _ ⇒
True
end
| LowvalBlock (Generative (Some bid1)) tag1 vs1 _ ⇒
match lv2 with
| LowvalBlock (Generative (Some bid2)) tag2 vs2 _ ⇒
bid1 ≠ bid2 ∨
tag1 ≠ tag2 ∨
vs1 ≠ vs2
| _ ⇒
True
end
| _ ⇒
True
end.
#[global] Instance lowvalｰnonsimilarｰdec :
RelDecision (≉@{lowval}).
#[global] Instance lowval۰similar : Similar lowval :=
fix go lv1 lv2 :=
match lv1 with
| LowvalLit llit1 ⇒
lv2 = LowvalLit llit1
| LowvalRecs ⇒
lv2 = LowvalRecs
| LowvalBlock gen1 tag1 vs1 lvs1 ⇒
match lv2 with
| LowvalBlock gen2 tag2 vs2 lvs2 ⇒
match gen1, gen2 with
| Generative bid1, Generative bid2 ⇒
bid1 = bid2 ∧
tag1 = tag2 ∧
vs1 = vs2
| Nongenerative, Nongenerative ⇒
tag1 = tag2 ∧
Forall2' go lvs1 lvs2
| _, _ ⇒
False
end
| _ ⇒
False
end
end.
#[global] Instance lowvalｰsimilarｰdec :
RelDecision (≈@{lowval}).
#[global] Instance lowvalｰnonsimilarｰsymmetric :
Symmetric (≉@{lowval}).
#[global] Instance lowvalｰsimilarｰreflexive :
Reflexive (≈@{lowval}).
Lemma lowvalｰsimilarｰrefl lv1 lv2 :
lv1 = lv2 →
lv1 ≈ lv2.
#[global] Instance lowvalｰsimilarｰsymmetric :
Symmetric (≈@{lowval}).
#[global] Instance lowvalｰsimilarｰtransitive :
Transitive (≈@{lowval}).
Lemma lowvalｰsimilarｰorｰnonsimilar lv1 lv2 :
lv1 ≈ lv2 ∨ lv1 ≉ lv2.
Lemma lowvalｰnonsimilarｰsimilar lv1 lv2 lv3 :
lv1 ≉ lv2 →
lv2 ≈ lv3 →
lv1 ≉ lv3.
#[global] Instance val۰nonsimilar : Nonsimilar val :=
λ v1 v2,
val۰to_low v1 ≉ val۰to_low v2.
#[global] Instance valｰnonsimilarｰdec : RelDecision (≉@{val}) :=
ltac:(rewrite /nonsimilar /val۰nonsimilar; solve_decision).
#[global] Instance val۰similar : Similar val :=
λ v1 v2,
val۰to_low v1 ≈ val۰to_low v2.
#[global] Instance valｰsimilarｰdec : RelDecision (≈@{val}) :=
ltac:(rewrite /similar /val۰similar; solve_decision).
#[global] Instance valｰnonsimilarｰsymmetric :
Symmetric (≉@{val}).
Lemma valｰnonsimilarｰbool b1 b2 :
ValBool b1 ≉ ValBool b2 →
b1 ≠ b2.
Lemma valｰnonsimilarｰint n1 n2 :
ValInt n1 ≉ ValInt n2 →
n1 ≠ n2.
Lemma valｰnonsimilarｰnat (n1 n2 : nat) :
ValNat n1 ≉ ValNat n2 →
n1 ≠ n2.
Lemma valｰnonsimilarｰlocation l1 l2 :
ValLoc l1 ≉ ValLoc l2 →
l1 ≠ l2.
Lemma valｰnonsimilarｰblockｰempty gen1 tag1 gen2 tag2 :
ValBlock gen1 tag1 [] ≉ ValBlock gen2 tag2 [] →
tag1 ≠ tag2.
Lemma valｰnonsimilarｰblockｰgenerative bid1 tag1 vs1 bid2 tag2 vs2 :
tag1 = tag2 →
vs1 = vs2 →
ValBlock (Generative (Some bid1)) tag1 vs1 ≉ ValBlock (Generative (Some bid2)) tag2 vs2 →
length vs1 = 0 ∨ bid1 ≠ bid2.
#[global] Instance valｰsimilarｰreflexive :
Reflexive (≈@{val}).
Lemma valｰsimilarｰrefl v1 v2 :
v1 = v2 →
v1 ≈ v2.
#[global] Instance valｰsimilarｰsymmetric :
Symmetric (≈@{val}).
#[global] Instance valｰsimilarｰtransitive :
Transitive (≈@{val}).
Lemma valｰsimilarｰbool b1 b2 :
ValLit (LitBool b1) ≈ ValLit (LitBool b2) →
b1 = b2.
Lemma valｰsimilarｰint n1 n2 :
ValLit (LitInt n1) ≈ ValLit (LitInt n2) →
n1 = n2.
Lemma valｰsimilarｰnat (n1 n2 : nat) :
ValLit (LitInt n1) ≈ ValLit (LitInt n2) →
n1 = n2.
Lemma valｰsimilarｰlocation l1 l2 :
ValLit (LitLoc l1) ≈ ValLit (LitLoc l2) →
l1 = l2.
Lemma valｰsimilarｰblockｰempty gen1 tag1 gen2 tag2 :
ValBlock gen1 tag1 [] ≈ ValBlock gen2 tag2 [] →
tag1 = tag2.
Lemma valｰsimilarｰblockｰempty₁ gen1 tag1 gen2 tag2 v2 vs2 :
¬ ValBlock gen1 tag1 [] ≈ ValBlock gen2 tag2 (v2 :: vs2).
Lemma valｰsimilarｰblockｰempty₂ gen1 tag1 v1 vs1 gen2 tag2 :
¬ ValBlock gen1 tag1 (v1 :: vs1) ≈ ValBlock gen2 tag2 [].
Lemma valｰsimilarｰblockｰgenerative bid1 tag1 vs1 bid2 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
ValBlock (Generative bid1) tag1 vs1 ≈ ValBlock (Generative bid2) tag2 vs2 →
bid1 = bid2 ∧
tag1 = tag2 ∧
vs1 = vs2.
Lemma valｰsimilarｰblockｰnongenerative tag1 vs1 tag2 vs2 :
ValBlock Nongenerative tag1 vs1 ≈ ValBlock Nongenerative tag2 vs2 →
tag1 = tag2 ∧
length vs1 = length vs2.
Lemma valｰsimilarｰlocationｰblock l gen tag vs :
¬ ValLit (LitLoc l) ≈ ValBlock gen tag vs.
Lemma valｰsimilarｰblockｰlocation gen tag vs l :
¬ ValBlock gen tag vs ≈ ValLit (LitLoc l).
Lemma valｰsimilarｰblockｰgenerativeｰnongenerative bid1 tag1 vs1 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
¬ ValBlock (Generative bid1) tag1 vs1 ≈ ValBlock Nongenerative tag2 vs2.
Lemma valｰsimilarｰblockｰnongenerativeｰgenerative tag1 vs1 bid2 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
¬ ValBlock Nongenerative tag1 vs1 ≈ ValBlock (Generative bid2) tag2 vs2.
Lemma valｰsimilarｰorｰnonsimilar v1 v2 :
v1 ≈ v2 ∨ v1 ≉ v2.
Lemma valｰnonsimilarｰsimilar v1 v2 v3 :
v1 ≉ v2 →
v2 ≈ v3 →
v1 ≉ v3.
Require Export zoo.common.typeclasses.
Require Export zoo.common.math.
Require Export zoo.common.list.
Require Export zoo.language.syntax.
Require Import zoo.options.
Implicit Type i tag : nat.
Implicit Type n : Z.
Implicit Type l : location.
Implicit Type gen : generativity.
Implicit Type lit : literal.
Implicit Type v : val.
Implicit Type vs : list val.
Variant lowliteral :=
| LowlitInt n
| LowlitLoc l
| LowlitProph
| LowlitPoison.
Implicit Type llit : lowliteral.
#[global] Instance lowliteralｰeq_dec : EqDecision lowliteral :=
ltac:(solve_decision).
Definition literal۰to_low lit :=
match lit with
| LitBool b ⇒
LowlitInt (Nat.b2n b)
| LitInt n ⇒
LowlitInt n
| LitLoc l ⇒
LowlitLoc l
| LitProph _ ⇒
LowlitProph
| LitPoison ⇒
LowlitPoison
end.
#[global] Arguments literal۰to_low !_ / : simpl nomatch, assert.
#[global] Instance lowliteral۰nonsimilar : Nonsimilar lowliteral :=
λ llit1 llit2,
match llit1 with
| LowlitInt n1 ⇒
llit2 ≠ LowlitInt n1
| LowlitLoc l1 ⇒
llit2 ≠ LowlitLoc l1
| _ ⇒
True
end.
#[global] Instance lowliteralｰnonsimilarｰdec :
RelDecision (≉@{lowliteral}).
#[global] Instance lowliteralｰnonsimilarｰsymmetric :
Symmetric (≉@{lowliteral}).
Inductive lowval :=
| LowvalLit llit
| LowvalRecs
| LowvalBlock gen tag vs (lvs : list lowval).
Implicit Type lv : lowval.
Implicit Type lvs : list lowval.
Section lowval۰ind.
Variable P : lowval → Prop.
Variable HLit :
∀ llit,
P (LowvalLit llit).
Variable HRecs :
P LowvalRecs.
Variable HBlock :
∀ gen tag vs,
∀ lvs, Forall P lvs →
P (LowvalBlock gen tag vs lvs).
Fixpoint lowval۰ind lv :=
match lv with
| LowvalLit llit ⇒
HLit
llit
| LowvalRecs ⇒
HRecs
| LowvalBlock gen tag vs lvs ⇒
HBlock
gen tag vs
lvs (Forall_true P lvs lowval۰ind)
end.
End lowval۰ind.
Notation LowvalInt n := (
LowvalLit (LowlitInt n)
)(only parsing
).
Notation LowvalLoc l := (
LowvalLit (LowlitLoc l)
)(only parsing
).
Notation LowvalProph := (
LowvalLit LowlitProph
)(only parsing
).
Notation LowvalPoison := (
LowvalLit LowlitPoison
)(only parsing
).
#[global] Instance lowvalｰeq_dec : EqDecision lowval.
Fixpoint val۰to_low v :=
match v with
| ValLit llit ⇒
LowvalLit (literal۰to_low llit)
| ValRecs _ _ ⇒
LowvalRecs
| ValBlock _ tag [] ⇒
LowvalLit (LowlitInt tag)
| ValBlock gen tag vs ⇒
LowvalBlock gen tag vs (val۰to_low <$> vs)
end.
#[global] Arguments val۰to_low !_ / : simpl nomatch, assert.
#[global] Instance lowval۰nonsimilar : Nonsimilar lowval :=
λ lv1 lv2,
match lv1 with
| LowvalLit llit1 ⇒
match lv2 with
| LowvalLit llit2 ⇒
llit1 ≉ llit2
| _ ⇒
True
end
| LowvalBlock (Generative (Some bid1)) tag1 vs1 _ ⇒
match lv2 with
| LowvalBlock (Generative (Some bid2)) tag2 vs2 _ ⇒
bid1 ≠ bid2 ∨
tag1 ≠ tag2 ∨
vs1 ≠ vs2
| _ ⇒
True
end
| _ ⇒
True
end.
#[global] Instance lowvalｰnonsimilarｰdec :
RelDecision (≉@{lowval}).
#[global] Instance lowval۰similar : Similar lowval :=
fix go lv1 lv2 :=
match lv1 with
| LowvalLit llit1 ⇒
lv2 = LowvalLit llit1
| LowvalRecs ⇒
lv2 = LowvalRecs
| LowvalBlock gen1 tag1 vs1 lvs1 ⇒
match lv2 with
| LowvalBlock gen2 tag2 vs2 lvs2 ⇒
match gen1, gen2 with
| Generative bid1, Generative bid2 ⇒
bid1 = bid2 ∧
tag1 = tag2 ∧
vs1 = vs2
| Nongenerative, Nongenerative ⇒
tag1 = tag2 ∧
Forall2' go lvs1 lvs2
| _, _ ⇒
False
end
| _ ⇒
False
end
end.
#[global] Instance lowvalｰsimilarｰdec :
RelDecision (≈@{lowval}).
#[global] Instance lowvalｰnonsimilarｰsymmetric :
Symmetric (≉@{lowval}).
#[global] Instance lowvalｰsimilarｰreflexive :
Reflexive (≈@{lowval}).
Lemma lowvalｰsimilarｰrefl lv1 lv2 :
lv1 = lv2 →
lv1 ≈ lv2.
#[global] Instance lowvalｰsimilarｰsymmetric :
Symmetric (≈@{lowval}).
#[global] Instance lowvalｰsimilarｰtransitive :
Transitive (≈@{lowval}).
Lemma lowvalｰsimilarｰorｰnonsimilar lv1 lv2 :
lv1 ≈ lv2 ∨ lv1 ≉ lv2.
Lemma lowvalｰnonsimilarｰsimilar lv1 lv2 lv3 :
lv1 ≉ lv2 →
lv2 ≈ lv3 →
lv1 ≉ lv3.
#[global] Instance val۰nonsimilar : Nonsimilar val :=
λ v1 v2,
val۰to_low v1 ≉ val۰to_low v2.
#[global] Instance valｰnonsimilarｰdec : RelDecision (≉@{val}) :=
ltac:(rewrite /nonsimilar /val۰nonsimilar; solve_decision).
#[global] Instance val۰similar : Similar val :=
λ v1 v2,
val۰to_low v1 ≈ val۰to_low v2.
#[global] Instance valｰsimilarｰdec : RelDecision (≈@{val}) :=
ltac:(rewrite /similar /val۰similar; solve_decision).
#[global] Instance valｰnonsimilarｰsymmetric :
Symmetric (≉@{val}).
Lemma valｰnonsimilarｰbool b1 b2 :
ValBool b1 ≉ ValBool b2 →
b1 ≠ b2.
Lemma valｰnonsimilarｰint n1 n2 :
ValInt n1 ≉ ValInt n2 →
n1 ≠ n2.
Lemma valｰnonsimilarｰnat (n1 n2 : nat) :
ValNat n1 ≉ ValNat n2 →
n1 ≠ n2.
Lemma valｰnonsimilarｰlocation l1 l2 :
ValLoc l1 ≉ ValLoc l2 →
l1 ≠ l2.
Lemma valｰnonsimilarｰblockｰempty gen1 tag1 gen2 tag2 :
ValBlock gen1 tag1 [] ≉ ValBlock gen2 tag2 [] →
tag1 ≠ tag2.
Lemma valｰnonsimilarｰblockｰgenerative bid1 tag1 vs1 bid2 tag2 vs2 :
tag1 = tag2 →
vs1 = vs2 →
ValBlock (Generative (Some bid1)) tag1 vs1 ≉ ValBlock (Generative (Some bid2)) tag2 vs2 →
length vs1 = 0 ∨ bid1 ≠ bid2.
#[global] Instance valｰsimilarｰreflexive :
Reflexive (≈@{val}).
Lemma valｰsimilarｰrefl v1 v2 :
v1 = v2 →
v1 ≈ v2.
#[global] Instance valｰsimilarｰsymmetric :
Symmetric (≈@{val}).
#[global] Instance valｰsimilarｰtransitive :
Transitive (≈@{val}).
Lemma valｰsimilarｰbool b1 b2 :
ValLit (LitBool b1) ≈ ValLit (LitBool b2) →
b1 = b2.
Lemma valｰsimilarｰint n1 n2 :
ValLit (LitInt n1) ≈ ValLit (LitInt n2) →
n1 = n2.
Lemma valｰsimilarｰnat (n1 n2 : nat) :
ValLit (LitInt n1) ≈ ValLit (LitInt n2) →
n1 = n2.
Lemma valｰsimilarｰlocation l1 l2 :
ValLit (LitLoc l1) ≈ ValLit (LitLoc l2) →
l1 = l2.
Lemma valｰsimilarｰblockｰempty gen1 tag1 gen2 tag2 :
ValBlock gen1 tag1 [] ≈ ValBlock gen2 tag2 [] →
tag1 = tag2.
Lemma valｰsimilarｰblockｰempty₁ gen1 tag1 gen2 tag2 v2 vs2 :
¬ ValBlock gen1 tag1 [] ≈ ValBlock gen2 tag2 (v2 :: vs2).
Lemma valｰsimilarｰblockｰempty₂ gen1 tag1 v1 vs1 gen2 tag2 :
¬ ValBlock gen1 tag1 (v1 :: vs1) ≈ ValBlock gen2 tag2 [].
Lemma valｰsimilarｰblockｰgenerative bid1 tag1 vs1 bid2 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
ValBlock (Generative bid1) tag1 vs1 ≈ ValBlock (Generative bid2) tag2 vs2 →
bid1 = bid2 ∧
tag1 = tag2 ∧
vs1 = vs2.
Lemma valｰsimilarｰblockｰnongenerative tag1 vs1 tag2 vs2 :
ValBlock Nongenerative tag1 vs1 ≈ ValBlock Nongenerative tag2 vs2 →
tag1 = tag2 ∧
length vs1 = length vs2.
Lemma valｰsimilarｰlocationｰblock l gen tag vs :
¬ ValLit (LitLoc l) ≈ ValBlock gen tag vs.
Lemma valｰsimilarｰblockｰlocation gen tag vs l :
¬ ValBlock gen tag vs ≈ ValLit (LitLoc l).
Lemma valｰsimilarｰblockｰgenerativeｰnongenerative bid1 tag1 vs1 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
¬ ValBlock (Generative bid1) tag1 vs1 ≈ ValBlock Nongenerative tag2 vs2.
Lemma valｰsimilarｰblockｰnongenerativeｰgenerative tag1 vs1 bid2 tag2 vs2 :
length vs1 ≠ 0 ∨ length vs2 ≠ 0 →
¬ ValBlock Nongenerative tag1 vs1 ≈ ValBlock (Generative bid2) tag2 vs2.
Lemma valｰsimilarｰorｰnonsimilar v1 v2 :
v1 ≈ v2 ∨ v1 ≉ v2.
Lemma valｰnonsimilarｰsimilar v1 v2 v3 :
v1 ≉ v2 →
v2 ≈ v3 →
v1 ≉ v3.