Ssreflect Users Discussion List

[Benjamin Werner <>]

I found this. I did not try how far it is efficient but
the definitions go through.

It certainly is quite ugly. It worked for not too complicated goals.


グ−ド　ラ−ック !

Benjamin


Require Import Omega.
Require Import finrel.
Require Import ssreflect.
Require Import ssrnat.
Require Import ssrbool.

Lemma  tr_or : forall x y, x || y <->  x \/ y.
move => x y; split.
 move/orP => [h|h]; [left|right]; done.
move => [h|h]; apply/orP; [left|right]; done.
Qed.

Lemma tr_and : forall x y, x && y <-> x /\ y.
move => x y; split.
 move/andP => [h1 h2]; split; done.
move => [h1 h2]; apply/andP; split; done.
Qed.

Lemma tr_not : forall x, negb x <-> ~x.
move => x; split.
 move/negP => h; done.
move=>h; apply/negP; done.
Qed.

Lemma tr_false : false <-> False.
Proof. intuition. Qed.

Lemma tr_true : true <-> True.
Proof. intuition. Qed.

Lemma tr_not_not : ~False <-> True.
Proof.  intuition. Qed.

Lemma tr_not_tr : ~True <-> False.
Proof. intuition. Qed.

Lemma tr_le : forall n m, n<=m <-> (le n m).
move => n m; split.
 by move/leP => h.
by move => h; apply/leP.
Qed.

Lemma tr_andFl : forall P, False/\P <-> False.
Proof. intuition. Qed.

Lemma tr_andFr : forall P, P/\False <-> False.
Proof. intuition. Qed.

Lemma tr_andTl : forall P, True/\P <-> P.
Proof. intuition. Qed.

Lemma tr_andTr : forall P, P/\True <-> P.
Proof. intuition. Qed.

Lemma tr_orFl : forall P, False\/P <-> P.
Proof. intuition. Qed.

Lemma tr_orFr : forall P, P\/False <-> P.
Proof. intuition. Qed.

Lemma tr_impFl : forall P : Prop, (False -> P) <-> True.
Proof. intuition. Qed.


Lemma tr_impTl : forall P:Prop, (True -> P) <-> P.
Proof. intuition. Qed.

Lemma tr_impTr : forall P:Prop, (P -> True) <-> True.
Proof. intuition. Qed.

Lemma tr_simp1 : ~True <-> False.
Proof. intuition. Qed.

Ltac tr_all :=
 do 3 (rewrite ?negb_orb ?negb_andb);
 rewrite /addn;
  do 3 (rewrite ?tr_or ?tr_and ?tr_not ?tr_true ?tr_false
        ?tr_not_not ?tr_simp1
        ?tr_not_tr ?tr_le ?tr_andFl ? tr_andFr ?tr_orFl ?tr_orFr ? 
tr_impFl ?tr_impTl
        ?tr_impTr ? tr_andTr ?tr_andTl).

Ltac myo := tr_all; trivial; intros; omega.







Le 8 déc. 08 à 13:09, <> <. 
jp> a écrit :

> Hello,
>
> If I decided to use ssrnat, then I have to give up the omega tactic?
>
> Best regards,
> Keiko