Commit 7aed832c authored by Glen Mével's avatar Glen Mével
Browse files

fix proof that expr is countable

parent d0ecd1fe
......@@ -459,7 +459,6 @@ Module base.
Qed.
Instance expr_countable : Countable expr.
Proof.
(*
set (enc :=
fix go e :=
match e with
......@@ -476,11 +475,12 @@ Module base.
| InjL e => GenNode 9 [go e]
| InjR e => GenNode 10 [go e]
| Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
| Read a e => GenNode 12 [GenLeaf (inr (inl (inl a))); go e]
| Write a e1 e2 => GenNode 13 [GenLeaf (inr (inl (inl a))); go e1; go e2]
| CAS e0 e1 e2 => GenNode 14 [go e0; go e1; go e2]
| Alloc a e => GenNode 15 [GenLeaf (inr (inl (inl a))); go e]
| Fork e => GenNode 16 [go e]
| Read a e ei => GenNode 12 [GenLeaf (inr (inl (inl a))); go e; go ei]
| Write a e ei e => GenNode 13 [GenLeaf (inr (inl (inl a))); go e; go ei; go e]
| CAS e ei e1 e2 => GenNode 14 [go e; go ei; go e1; go e2]
| Length e => GenNode 15 [go e]
| Alloc a ei e => GenNode 16 [GenLeaf (inr (inl (inl a))); go ei; go e]
| Fork e => GenNode 17 [go e]
end
with gov v :=
match v with
......@@ -508,11 +508,12 @@ Module base.
| GenNode 9 [e] => InjL (go e)
| GenNode 10 [e] => InjR (go e)
| GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
| GenNode 12 [GenLeaf (inr (inl (inl a))); e] => Read a (go e)
| GenNode 13 [GenLeaf (inr (inl (inl a))); e1; e2] => Write a (go e1) (go e2)
| GenNode 14 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 15 [GenLeaf (inr (inl (inl a))); e] => Alloc a (go e)
| GenNode 16 [e] => Fork (go e)
| GenNode 12 [GenLeaf (inr (inl (inl a))); e; ei] => Read a (go e) (go ei)
| GenNode 13 [GenLeaf (inr (inl (inl a))); e; ei; e] => Write a (go e) (go ei) (go e)
| GenNode 14 [e; ei; e1; e2] => CAS (go e) (go ei) (go e1) (go e2)
| GenNode 15 [e] => Length (go e)
| GenNode 16 [GenLeaf (inr (inl (inl a))); ei; e] => Alloc a (go ei) (go e)
| GenNode 17 [e] => Fork (go e)
| _ => Val $ LitV LitUnit (* dummy *)
end
with gov x :=
......@@ -527,12 +528,10 @@ Module base.
for go).
refine (inj_countable' enc dec _).
refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- destruct e as [v| | | | | | | | | | | | | | | | |]; simpl; f_equal;
- destruct e as [v| | | | | | | | | | | | | | | | | |]; simpl; f_equal;
[exact (gov v)|done..].
- destruct v; by f_equal.
Qed.
*)
Admitted.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. 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