Mercurial > cpdt > repo

comparison src/MoreDep.v @ 569:0ce9829efa3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 1dc1d41620b6
comparison
equal deleted inserted replaced
568:81d63d9c1cc5 569:0ce9829efa3b
645 | Black => fun r => r 645 | Black => fun r => r
646 end. 646 end.
647 647
648 (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *) 648 (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *)
649 649
650 Arguments makeRbtree [c n]. 650 Arguments makeRbtree [c n] _.
651 651
652 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *) 652 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
653 653
654 Definition insert c n (t : rbtree c n) : insertResult c n := 654 Definition insert c n (t : rbtree c n) : insertResult c n :=
655 makeRbtree (ins t). 655 makeRbtree (ins t).
915 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}. 915 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
916 refine (Reduce (split' (n := length s) _)); crush; eauto. 916 refine (Reduce (split' (n := length s) _)); crush; eauto.
917 Defined. 917 Defined.
918 End split. 918 End split.
919 919
920 Arguments split [P1 P2]. 920 Arguments split [P1 P2] P1_dec P2_dec s.
921 921
922 (* begin hide *) 922 (* begin hide *)
923 Lemma app_empty_end : forall s, s ++ "" = s. 923 Lemma app_empty_end : forall s, s ++ "" = s.
924 induction s; crush. 924 induction s; crush.
925 Qed. 925 Qed.