aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Add equivalence classesYann Herklotz2023-07-111-0/+2
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-261-3/+45
* Add SMTCoq solver as dependencyYann Herklotz2023-06-211-3/+3
* Finish complete evaluability proofYann Herklotz2023-06-101-19/+88
* Try to prove main theoremYann Herklotz2023-06-101-0/+5
* Add more to proof of evaluabilityYann Herklotz2023-06-101-0/+52
* Finish abstract_sequence_evaluable_mYann Herklotz2023-06-091-1/+104
* Prove abstract_sequence_evaluableYann Herklotz2023-06-091-0/+2
* Finish abstract_sequence_evaluable_fold2Yann Herklotz2023-06-091-5/+42
* Finish abstract_sequence_evaluable_foldYann Herklotz2023-06-091-12/+68
* Add outline of proof of evaluable when predicate is falseYann Herklotz2023-06-091-19/+54
* Add proof outline for evaluabilityYann Herklotz2023-06-081-18/+44
* Work towards proving evaluabilityYann Herklotz2023-06-051-1/+114
* Finished painful product proofYann Herklotz2023-05-301-4/+4
* Rename backwards proofYann Herklotz2023-05-121-30/+4
* Split proof up into more filesYann Herklotz2023-05-091-2006/+79
* Add assumption and prove assumption that preds are evaluableYann Herklotz2023-05-061-0/+1
* Add check for mutexcl and fix top-level proofYann Herklotz2023-05-061-18/+33
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-051-90/+0
* Change nat to positive in Sat proofYann Herklotz2023-04-271-8/+4
* Added lemmas about decidability of SatYann Herklotz2023-04-241-21/+0
* Work on proof of norm_expressionYann Herklotz2023-02-221-48/+0
* Remove aborted evaluable proofsYann Herklotz2023-02-181-96/+4
* Prove abstr_fold_falsy correctYann Herklotz2023-02-121-21/+100
* Prove sem_update_instr_term correctYann Herklotz2023-02-121-8/+19
* Prove abstr_fold_correct inductive case fullyYann Herklotz2023-02-121-12/+15
* Finish eval_predf_update_trueYann Herklotz2023-02-121-3/+6
* Finish sem_update_instr finallyYann Herklotz2023-02-121-3/+247
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-111-84/+52
* Switch to half lazy evaluationYann Herklotz2023-02-051-43/+84
* Work on intermediate lemma for evaluationYann Herklotz2023-01-291-5/+12
* Prove abstr_fold_correct top-downYann Herklotz2023-01-291-41/+94
* Add documentation and continue on top-down proofYann Herklotz2023-01-281-6/+54
* Work on simplifying seq_app evaluation lemmaYann Herklotz2023-01-021-6/+11
* Add all_evaluable lemma for seq_appYann Herklotz2023-01-011-0/+9
* Add proofs about evaluation of body of expressionsYann Herklotz2022-12-271-7/+59
* Add proofs about evaluability of predicates in the abstract stateYann Herklotz2022-12-241-23/+55
* Add todoYann Herklotz2022-12-011-76/+163
* Prove top level theorems with evaluabilityYann Herklotz2022-11-151-43/+333
* Add proofs about evaluability of predicatesYann Herklotz2022-11-101-18/+132
* Add many more proofs about sem_pred_exprYann Herklotz2022-10-261-36/+311
* Add proofs for sem_pexpr and app_predicatedYann Herklotz2022-10-251-43/+269
* Prove sem_update for load and create lemmaYann Herklotz2022-10-241-3/+51
* Work on abstract lemmas for update functionYann Herklotz2022-10-201-8/+318
* Clean up proofsYann Herklotz2022-10-111-11/+31
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-061-842/+113
* Add global monad notation using InstancesYann Herklotz2022-09-261-83/+75
* Update and fix the transformationYann Herklotz2022-08-051-252/+253
* Update lemmas with new update functionYann Herklotz2022-07-261-35/+128
* Fix main proofYann Herklotz2022-07-201-21/+27
generated by cgit (git 2.34.1) at 2024-06-26 02:37:13 +0000