Many hyperlinks are disabled.

Use anonymous login
to enable hyperlinks.

Overview

Comment: | Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. |
---|---|

Downloads: | Tarball | ZIP archive | SQL archive |

Timelines: | family | ancestors | descendants | both | trunk |

Files: | files | file ages | folders |

SHA1: | 95a716e7e5720454efda602616362f2c32281dad |

User & Date: | andy 2015-04-18 16:44:05 |

Context

2015-04-18
| ||

16:44 | Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk | |

16:44 | Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk | |

2015-04-16
| ||

22:02 | Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk | |

Changes

Changes to plsrc/nat_spec_demo.pl.

9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 |
spec([ % Due to an oversight on my part, the way we handle inductive proofs, % although correct, will not work with the kind of incremental proofs % construction we are aiming to do. More permanent solutions will have to % come later, but for now we hard-code the IH into the specification. % (Which, yes, means that you can only prove one thing by induction!) ih('IH', add(' x', z, ' x'), 'nat|sml'(' x')), % Nat formation rules rule('Nat-z', nat(z), and([true])), rule('Nat-succ', nat(s(' n')), and([nat(' n')])), % Addition rules rule('Add-z', add(z,' x', ' x'), and([true])), |
| |
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 |
spec([ % Due to an oversight on my part, the way we handle inductive proofs, % although correct, will not work with the kind of incremental proofs % construction we are aiming to do. More permanent solutions will have to % come later, but for now we hard-code the IH into the specification. % (Which, yes, means that you can only prove one thing by induction!) ih('IH', add(' x', z, ' x'), and(['nat|sml'(' x')])), % Nat formation rules rule('Nat-z', nat(z), and([true])), rule('Nat-succ', nat(s(' n')), and([nat(' n')])), % Addition rules rule('Add-z', add(z,' x', ' x'), and([true])), |