Mercurial > cpdt > repo
comparison src/Equality.v @ 569:0ce9829efa3b
Back to working in Coq 8.4
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2019 15:28:23 -0500 |
parents | 81d63d9c1cc5 |
children |
comparison
equal
deleted
inserted
replaced
568:81d63d9c1cc5 | 569:0ce9829efa3b |
---|---|
212 | inr idx' => fhget ls' (snd mls) idx' | 212 | inr idx' => fhget ls' (snd mls) idx' |
213 end | 213 end |
214 end. | 214 end. |
215 End fhlist. | 215 End fhlist. |
216 | 216 |
217 Arguments fhget [A B elm ls]. | 217 Arguments fhget [A B elm ls] _ _. |
218 | 218 |
219 (* begin hide *) | 219 (* begin hide *) |
220 (* begin thide *) | 220 (* begin thide *) |
221 Definition map := O. | 221 Definition map := O. |
222 (* end thide *) | 222 (* end thide *) |
233 match ls return fhlist B ls -> fhlist C ls with | 233 match ls return fhlist B ls -> fhlist C ls with |
234 | nil => fun _ => tt | 234 | nil => fun _ => tt |
235 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls)) | 235 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls)) |
236 end. | 236 end. |
237 | 237 |
238 Arguments fhmap [ls]. | 238 Arguments fhmap [ls] _. |
239 | 239 |
240 (* begin hide *) | 240 (* begin hide *) |
241 (* begin thide *) | 241 (* begin thide *) |
242 Definition ilist := O. | 242 Definition ilist := O. |
243 Definition get := O. | 243 Definition get := O. |
494 match ls1 with | 494 match ls1 with |
495 | nil => fun _ hls2 => hls2 | 495 | nil => fun _ hls2 => hls2 |
496 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) | 496 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) |
497 end. | 497 end. |
498 | 498 |
499 Arguments fhapp [ls1 ls2]. | 499 Arguments fhapp [ls1 ls2] _ _. |
500 | 500 |
501 (* EX: Prove that fhapp is associative. *) | 501 (* EX: Prove that fhapp is associative. *) |
502 (* begin thide *) | 502 (* begin thide *) |
503 | 503 |
504 (** We might like to prove that [fhapp] is associative. | 504 (** We might like to prove that [fhapp] is associative. |
674 reflexivity. | 674 reflexivity. |
675 Qed. | 675 Qed. |
676 (* end thide *) | 676 (* end thide *) |
677 End fhapp. | 677 End fhapp. |
678 | 678 |
679 Arguments fhapp [A B ls1 ls2]. | 679 Arguments fhapp [A B ls1 ls2] _ _. |
680 | 680 |
681 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *) | 681 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *) |
682 | 682 |
683 | 683 |
684 (** * Heterogeneous Equality *) | 684 (** * Heterogeneous Equality *) |