Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents f83664d817ce
children 8077352044b2
comparison
equal deleted inserted replaced
425:6ed5ee4845e4 426:5f25705a10ea
330 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst 330 case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst
331 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in 331 | [ _ : context[match ?M with exist _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in
332 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst 332 case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
333 | [ H : forall n v, ?E n = Some v -> _, 333 | [ H : forall n v, ?E n = Some v -> _,
334 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] => 334 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
335 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate 335 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
336 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto 336 | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
337 end; simpl in *); eauto 7. 337 end; simpl in *); eauto 7.
338 338
339 Ltac run := run'; repeat (match goal with 339 Ltac run := run'; repeat (match goal with
340 | [ H : forall n v, ?E n = Some v -> _ 340 | [ H : forall n v, ?E n = Some v -> _
341 |- context[match ?E ?N with Some _ => _ | None => _ end] ] => 341 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
342 specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate 342 specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
343 end; run'). 343 end; run').
344 344
345 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P. 345 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
346 exists 0; auto. 346 exists 0; auto.
347 Qed. 347 Qed.
534 End Fix. 534 End Fix.
535 535
536 (* begin hide *) 536 (* begin hide *)
537 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y) 537 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
538 -> x = y. 538 -> x = y.
539 intros ? ? ? H; generalize (H _ (refl_equal _)); crush. 539 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
540 Qed. 540 Qed.
541 541
542 Lemma leq_None : forall A (x y : A), leq (Some x) None 542 Lemma leq_None : forall A (x y : A), leq (Some x) None
543 -> False. 543 -> False.
544 intros ? ? ? H; generalize (H _ (refl_equal _)); crush. 544 intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
545 Qed. 545 Qed.
546 546
547 Ltac mergeSort' := run; 547 Ltac mergeSort' := run;
548 repeat (match goal with 548 repeat (match goal with
549 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E 549 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E