## Mercurial > cpdt > repo

### comparison src/Large.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Builds with Coq 8.5beta2

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 05 Aug 2015 14:46:55 -0400 |

parents | 21079e42b773 |

children | dac7a2705b00 |

comparison

equal
deleted
inserted
replaced

533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|

1 (* Copyright (c) 2009-2012, Adam Chlipala | 1 (* Copyright (c) 2009-2012, 2015, Adam Chlipala |

2 * | 2 * |

3 * This work is licensed under a | 3 * This work is licensed under a |

4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |

5 * Unported License. | 5 * Unported License. |

6 * The license text is available at: | 6 * The license text is available at: |

8 *) | 8 *) |

9 | 9 |

10 (* begin hide *) | 10 (* begin hide *) |

11 Require Import Arith. | 11 Require Import Arith. |

12 | 12 |

13 Require Import CpdtTactics. | 13 Require Import Cpdt.CpdtTactics. |

14 | 14 |

15 Set Implicit Arguments. | 15 Set Implicit Arguments. |

16 Set Asymmetric Patterns. | |

16 (* end hide *) | 17 (* end hide *) |

17 | 18 |

18 | 19 |

19 (** %\part{The Big Picture} | 20 (** %\part{The Big Picture} |

20 | 21 |

388 t''. | 389 t''. |

389 Qed. | 390 Qed. |

390 | 391 |

391 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *) | 392 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *) |

392 | 393 |

393 Reset t. | 394 Reset cfold_correct. |

394 | 395 |

395 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). | 396 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). |

396 induction e; crush; | 397 induction e; crush; |

397 repeat (match goal with | 398 repeat (match goal with |

398 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => | 399 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => |