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.