I started tidying things a little bit and it snowballed into quite a few changes, hopefully for the best. Main changes are:
Change in the way we import files. The main constructions are imported at once with From CTree Require Import CTree. The main equational theory for equ and sbisim is obtained at once with From CTree Require Import Eq. For weak bisimulation, you should import manually From CTree Require Import Eq.WBisim.
Relations (equ, sbisim, wbisim) are now definitions and not notations so that in particular we can search for lemmas about them. Be careful to follow the import discipline described above to make sure you get in scope the tactics taking care of the necessary unfolding and folding.
Following @nchappe 's suggestion, I added a up-to Vis context and proved it sound for sbisim --- the tactic upto_vis is the simplest way to use it.
Provided a few other tactics:
upto_bind: application of an upto bind principle for equ or sbisim, in front of a gfp, t _ or bt _ goal. In the case of equ, introduce an evar for the intermediate relation.
upto_bind_eq: the same, but specifically for a goal where both prefixes are the same --- discharge them automatically with reflexivity
upto_bind with SS: for equ, provides the desired intermediate relation.
play/playL/playR/eplayL/eplayR to exploit sbisim hypotheses
etrans: automatic solving for trans --- Quite stupid, just a bunch of hint resolve.
Tried to make the naming conventions more consistent, so a fair bit of changes
trans does not reduce with cbn and simpl, making it necessary to unfold it manually sometimes. It's annoying, but very convenient for the automation, I'm not quite decided yet about this.
I started tidying things a little bit and it snowballed into quite a few changes, hopefully for the best. Main changes are:
From CTree Require Import CTree
. The main equational theory forequ
andsbisim
is obtained at once withFrom CTree Require Import Eq
. For weak bisimulation, you should import manuallyFrom CTree Require Import Eq.WBisim
.equ
,sbisim
,wbisim
) are now definitions and not notations so that in particular we can search for lemmas about them. Be careful to follow the import discipline described above to make sure you get in scope the tactics taking care of the necessary unfolding and folding.Vis
context and proved it sound forsbisim
--- the tacticupto_vis
is the simplest way to use it.upto_bind
: application of an upto bind principle forequ
orsbisim
, in front of agfp
,t _
orbt _
goal. In the case ofequ
, introduce an evar for the intermediate relation.upto_bind_eq
: the same, but specifically for a goal where both prefixes are the same --- discharge them automatically withreflexivity
upto_bind with SS
: forequ
, provides the desired intermediate relation.play/playL/playR/eplayL/eplayR
to exploitsbisim
hypothesesetrans
: automatic solving fortrans
--- Quite stupid, just a bunch of hint resolve.trans
does not reduce withcbn
andsimpl
, making it necessary to unfold it manually sometimes. It's annoying, but very convenient for the automation, I'm not quite decided yet about this.