Mercurial > cpdt > repo

comparison src/Equality.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents d65e9c1c9041
children 0ce9829efa3b
comparison
equal deleted inserted replaced
567:ec0ce5129fc4 568:81d63d9c1cc5
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 Implicit 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 Implicit 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 Implicit 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 Implicit 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 *)