Commits on Jun 26, 2023

1. lib: add corres_cases method …

   Add safe datatype case distinction for corres -- wpc turns out to be
   insufficient even after generalisation of the helper predicate.
   
   - corres_cases_left: case distinction on abstract monad
   - corres_cases_right: case distinction on concrete monad
   - corres_cases: try first corres_cases_left, then corres_cases_right
   - corres_cases_both: simultaneous (quadratic) case distinction on
     both sides, with safe elimination of trivially contradictory cases.
   
   Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

   

   lsf37 committed Jun 26, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 5abb456
   • Browse repository at this point

   Copy the full SHA

   5abb456 View commit details

   Browse the repository at this point in the history

2. crefine: remove obsolete corres wpc setup …

   This setup didn't actually work. Replaced by corres_cases.
   
   Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

   

   lsf37 committed Jun 26, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 168d3aa
   • Browse repository at this point

   Copy the full SHA

   168d3aa View commit details

   Browse the repository at this point in the history

3. arm refine: deploy corres_cases in some examples …

   Demonstrates use of corres_cases and corres_cases_both. Main intended
   benefit is less thinking about safety of schematics, fewer mentions
   of goal parameter names, and fewer manual guard instantiations.
   
   Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

   

   lsf37 committed Jun 26, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 59759ed
   • Browse repository at this point

   Copy the full SHA

   59759ed View commit details

   Browse the repository at this point in the history