ProofCafe/crush のバックアップ(No.1)

• バックアップ一覧
• ソース を表示
• ProofCafe/crush は削除されています。
  • 1 (2010-05-22 (土) 16:42:37)

ProofCafe

Ltac crush' lemmas invOne :=

 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
   let rewriter := autorewrite with cpdt in *;
     repeat (match goal with
               | [ H : _ |- _ ] => (rewrite H; [])
                 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
                   || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
             end; autorewrite with cpdt in *)
   in (sintuition; rewriter;
       match lemmas with
         | false => idtac
         | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
           repeat (simplHyp invOne; intuition)); un_done
       end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

Ltac crush := crush' false fail.