| Age | Commit message (Collapse) | Author |
|---|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing
|
|
Includes removing an explicit use of a lemma generated by abstract, which
was causing problems with different versions of Coq because the names
change.
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
- add state versions of foreach combinators
- support dependent sumbool pattern matching (i.e., those where the
property is actually used)
- add rewriting congruence rules, state monad lifting rules,
and invariant proof rules for these
|
|
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
|
|
|
|
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
|
|
|
|
|
|
* rename state fields to avoid clash with regstate type
* use rewriting to automate some proofs
|
|
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
|
|
|
|
|
