awalterschulze regex-reexamined-coq issues

awalterschulze / regex-reexamined-coq

Apache License 2.0

21 stars 7 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Automate proving of splitting of lists with exists aka concat

#189 awalterschulze opened 3 years ago
0
tactic state can now handle hypothesis and terms

#188 awalterschulze closed 3 years ago
0
dubstep using cbn

#187 awalterschulze closed 3 years ago
1
wreckit deconstructs the goal if it solves the goal

#186 awalterschulze closed 3 years ago
0
wreckit also inverts if there are zero goals as a result

#185 awalterschulze closed 3 years ago
0
use more wreckit in exampleR

#184 awalterschulze closed 3 years ago
0
wreckit tactic notation more in and as with simple_intropattern

#183 awalterschulze closed 3 years ago
0
wreckit with more notation in

#182 awalterschulze closed 3 years ago
0
wreckit exists with tactic notation in

#181 awalterschulze closed 3 years ago
0
move state into TacticState.v

#180 awalterschulze closed 3 years ago
0
Add inversion to wreckit

#179 Nielius closed 3 years ago
0
Adopt some of the crush tactic for more automated proving

#178 awalterschulze opened 3 years ago
1
rewrite using lang_iff in bisimilar

#177 awalterschulze closed 3 years ago
0
cofixpoint derive tree

#176 awalterschulze closed 3 years ago
0
coinduction trace for derivatives

#175 awalterschulze closed 3 years ago
0
derive function that should end in finite steps

#174 awalterschulze closed 3 years ago
0
more failed work on coinduction that increases the foundation

#173 awalterschulze closed 3 years ago
0
Rewriting between two setoids: bisimilar and lang_iff

#172 awalterschulze opened 3 years ago
0
star commutes and thus derive commutes

#171 awalterschulze closed 3 years ago
2
concat commutes

#170 awalterschulze closed 3 years ago
0
less unfolding and easier rewriting in commutes_a_concat

#169 awalterschulze closed 3 years ago
1
split Null.v into NullCommutes.v and Null.v

#168 awalterschulze closed 3 years ago
0
add setoid rewrite for derive_lang and derive_langs

#167 awalterschulze closed 3 years ago
0
flip order of parameters for derive_lang and change name

#166 awalterschulze closed 3 years ago
0
move derive commutes into separate file

#165 awalterschulze closed 3 years ago
0
concat_a commute step 1

#164 awalterschulze closed 3 years ago
0
move elem_morph

#163 awalterschulze closed 3 years ago
0
Add Parametric Morphism: elem_morph

#162 awalterschulze closed 3 years ago
0
finish semi ring and complete split empty str proof

#161 awalterschulze closed 3 years ago
1
Definition vs Inductive

#160 awalterschulze opened 3 years ago
7
change definition of and to be property based

#159 awalterschulze closed 3 years ago
1
changes proposed by niels in #149

#158 awalterschulze closed 3 years ago
1
a template to create an or_lang semi ring

#157 awalterschulze closed 3 years ago
1
split regular expression into itself and empty str

#156 awalterschulze closed 3 years ago
1
Update CI to Coq 8.13.0 and fix warnings

#155 paulcadman closed 3 years ago
0
Rewrite definition of and_lang

#154 awalterschulze closed 3 years ago
0
proof and is conj and some more simplification rules

#153 awalterschulze closed 3 years ago
1
replaced lambda by epsilon and emptystr

#152 awalterschulze closed 3 years ago
1
replace delta by nu and null

#151 awalterschulze closed 3 years ago
0
Bisimilar Setoid

#150 awalterschulze closed 3 years ago
0
replace nor with or + not

#149 awalterschulze closed 3 years ago
2
bisimilarity is equivalence

#148 awalterschulze closed 3 years ago
0
More auto for lists

#147 awalterschulze opened 3 years ago
0
Replace `elem` with \in and `notelem` with \notin

#146 paulcadman closed 3 years ago
1
Simpler Logical operators for Brzozowski than nor

#145 awalterschulze closed 3 years ago
9
pair programming results from past two sessions

#144 awalterschulze closed 3 years ago
0
Try Tactician

#143 awalterschulze opened 3 years ago
0
Try alectryon as a way to generate readable proofs

#142 awalterschulze opened 3 years ago
1
Cleaning up decidable

#141 awalterschulze closed 3 years ago
1
Move list theorems

#140 awalterschulze closed 3 years ago
0