← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/FSets/FSetDecide.v

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/FSets/FSetDecide.v
6
6
(*         *       GNU Lesser General Public License Version 2.1       *)
7
7
(***********************************************************************)
8
8
 
9
 
(* $Id: FSetDecide.v 13171 2010-06-18 21:45:40Z letouzey $ *)
 
9
(* $Id: FSetDecide.v 14527 2011-10-07 14:33:38Z letouzey $ *)
10
10
 
11
11
(**************************************************************)
12
12
(* FSetDecide.v                                               *)
368
368
      "else" tactic(t2) :=
369
369
      first [ t; first [ t1 | fail 2 ] | t2 ].
370
370
 
 
371
    Ltac abstract_term t :=
 
372
      if (is_var t) then fail "no need to abstract a variable"
 
373
      else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
374
 
 
375
    Ltac abstract_elements :=
 
376
      repeat
 
377
        (match goal with
 
378
           | |- context [ singleton ?t ] => abstract_term t
 
379
           | _ : context [ singleton ?t ] |- _ => abstract_term t
 
380
           | |- context [ add ?t _ ] => abstract_term t
 
381
           | _ : context [ add ?t _ ] |- _ => abstract_term t
 
382
           | |- context [ remove ?t _ ] => abstract_term t
 
383
           | _ : context [ remove ?t _ ] |- _ => abstract_term t
 
384
           | |- context [ In ?t _ ] => abstract_term t
 
385
           | _ : context [ In ?t _ ] |- _ => abstract_term t
 
386
         end).
 
387
 
371
388
    (** [prop P holds by t] succeeds (but does not modify the
372
389
        goal or context) if the proposition [P] can be proved by
373
390
        [t] in the current context.  Otherwise, the tactic
460
477
        tactic). *)
461
478
    Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
462
479
    Ltac discard_nonFSet :=
463
 
      decompose records;
464
480
      repeat (
465
481
        match goal with
 
482
        | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
 
483
          if (change T with E.t in H) then fail
 
484
          else if (change T with t in H) then fail
 
485
          else clear H
466
486
        | H : ?P |- _ =>
467
487
          if prop (FSet_Prop P) holds by
468
488
            (auto 100 with FSet_Prop)
482
502
      F.union_iff F.inter_iff F.diff_iff
483
503
    : set_simpl.
484
504
 
 
505
    Lemma eq_refl_iff (x : E.t) : E.eq x x <-> True.
 
506
    Proof.
 
507
     now split.
 
508
    Qed.
 
509
 
 
510
    Hint Rewrite eq_refl_iff : set_eq_simpl.
 
511
 
485
512
    (** ** Decidability of FSet Propositions *)
486
513
 
487
514
    (** [In] is decidable. *)
558
585
    Ltac substFSet :=
559
586
      repeat (
560
587
        match goal with
 
588
        | H: E.eq ?x ?x |- _ => clear H
561
589
        | H: E.eq ?x ?y |- _ => rewrite H in *; clear H
562
 
        end).
 
590
        end);
 
591
      autorewrite with set_eq_simpl in *.
563
592
 
564
593
    (** ** Considering Decidability of Base Propositions
565
594
        This tactic adds assertions about the decidability of
639
668
    (** Here is the crux of the proof search.  Recursion through
640
669
        [intuition]!  (This will terminate if I correctly
641
670
        understand the behavior of [intuition].) *)
642
 
    Ltac fsetdec_rec :=
643
 
      try (match goal with
644
 
      | H: E.eq ?x ?x -> False |- _ => destruct H
645
 
      end);
646
 
      (reflexivity ||
647
 
      contradiction ||
648
 
      (progress substFSet; intuition fsetdec_rec)).
 
671
    Ltac fsetdec_rec := progress substFSet; intuition fsetdec_rec.
649
672
 
650
673
    (** If we add [unfold Empty, Subset, Equal in *; intros;] to
651
674
        the beginning of this tactic, it will satisfy the same
653
676
        be much slower than necessary without the pre-processing
654
677
        done by the wrapper tactic [fsetdec]. *)
655
678
    Ltac fsetdec_body :=
 
679
      autorewrite with set_eq_simpl in *;
656
680
      inst_FSet_hypotheses;
657
 
      autorewrite with set_simpl in *;
 
681
      autorewrite with set_simpl set_eq_simpl in *;
658
682
      push not in * using FSet_decidability;
659
683
      substFSet;
660
684
      assert_decidability;
661
 
      auto using E.eq_refl;
 
685
      auto;
662
686
      (intuition fsetdec_rec) ||
663
687
      fail 1
664
688
        "because the goal is beyond the scope of this tactic".
677
701
        [intros] to leave us with a goal of [~ P] than a goal of
678
702
        [False]. *)
679
703
    fold any not; intros;
 
704
    (** We don't care about the value of elements : complex ones are
 
705
        abstracted as new variables (avoiding potential dependencies,
 
706
        see bug #2464) *)
 
707
    abstract_elements;
680
708
    (** We remove dependencies to logical hypothesis. This way,
681
709
        later "clear" will work nicely (see bug #2136) *)
682
710
    no_logical_interdep;
876
904
    the subtyping [WS<=S], the [Decide] functor which is meant to be
877
905
    used on modules [(M:S)] can simply be an alias of [WDecide]. *)
878
906
 
879
 
Module WDecide (M:WS) := WDecide_fun M.E M.
 
907
Module WDecide (M:WS) := !WDecide_fun M.E M.
880
908
Module Decide := WDecide.