source: etc/campbell/dev-notes/2012-04-04-flattening2.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 970 bytes
Line 
1The idea was to flatten the structured traces and show that these are the same
2as the original trace.  This looks like it could work out OK, but with the
3caveats that:
4
5  1. flattening is a not-quite trivial operations - we need to define a type
6     of finite flat traces to get out of the finite structured traces, get the
7     executable parts from Prop into Type[0] using their executability, then
8     define a careful pair of mutual cofixpoints to satisfy the guardedness
9     conditions;
10
11  2. we can't show the usual equality on coinductive data, so we need to define
12     a specialised coinductive equality predicate for flat traces; and
13
14  3. define a cofixpoint proof for that tediously going through all of the
15     structure I defined at 1 (this is the point that I'm at).
16
17After all of this, we get a corrollary saying the the flattened result of
18making a structured trace must be the same as the original trace because all
19traces from the same place are.
Note: See TracBrowser for help on using the repository browser.