-lemma max_n_O : ∀n. max n O = n. intros; cases n; reflexivity; qed.
-
-lemma min_n_n : ∀n. min n n = n. intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; qed.
-
-lemma min_le: ∀m,n. n ≤ m → min n m = n.
-intro; elim m; [cases n in H; intros; [reflexivity] cases (not_le_Sn_O ? H)]
-cases n1 in H1;
-
-
-lemma xxx : ∀a,b,c.min (min a b) c = min a (min b c).
-intros; elim a; [reflexivity] elim b in c H 0; [intros;reflexivity] intros;
-lapply depth=0 (H O);
-
-
-simplify in ⊢ (? ? ? (? ? %));
-simplify in ⊢ (? ? (? % ?) ?);
-simplify in H:(? ? (? % ?) ?);
-simplify in H:(? ? ? (? ? %));
-simplify in ⊢ (? ? ? %);reflexivity]
-simplify in ⊢ (? ? (? % ?) ?);reflexivity]
+definition invert ≝
+ λv:ℕ -> ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0.
+
+(*DOCBEGIN
+
+Il linguaggio di dimostrazione di Matita
+========================================
+
+Per dimostrare questo teorema in modo agevole è necessario utilizzare il
+seguente comando:
+
+* `symmetry`
+
+ Quando la conclusuine è `a = b` permette di cambiarla in `b = a`.
+
+DOCEND*)
+theorem negate_invert:
+ ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
+assume F:Formula.
+assume v:(ℕ→ℕ).
+we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)).
+ case FBot .
+ the thesis becomes ([[ negate FBot ]]_v=[[ FBot ]]_(invert v)).
+ done.
+ case FTop .
+ the thesis becomes ([[ negate FTop ]]_v=[[ FTop ]]_(invert v)).
+ done.
+ case FAtom.
+ assume n : ℕ.
+ the thesis becomes ([[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)).
+ the thesis becomes (1 - (min (v n) 1)= min (invert v n) 1).
+ the thesis becomes (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1).
+ by min_bool we proved (min (v n) 1 = 0 ∨ min (v n) 1 = 1) (H1);
+ we proceed by cases on (H1) to prove (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1).
+ case Left.
+ conclude
+ (1 - (min (v n) 1))
+ = (1 - 0) by H.
+ = 1.
+ symmetry.
+ conclude
+ (min (if eqb (min (v n) 1) O then 1 else O) 1)
+ = (min (if eqb 0 0 then 1 else O) 1) by H.
+ = (min 1 1).
+ = 1.
+ done.
+ case Right.
+ conclude
+ (1 - (min (v n) 1))
+ = (1 - 1) by H.
+ = 0.
+ symmetry.
+ conclude
+ (min (if eqb (min (v n) 1) O then 1 else O) 1)
+ = (min (if eqb 1 0 then 1 else O) 1) by H.
+ = (min 0 1).
+ = 0.
+ done.
+ case FAnd.
+ assume f : Formula.
+ by induction hypothesis we know
+ ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
+ assume f1 : Formula.
+ by induction hypothesis we know
+ ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1).
+ the thesis becomes
+ ([[ negate (FAnd f f1) ]]_v=[[ FAnd f f1 ]]_(invert v)).
+ the thesis becomes
+ (min [[ negate f ]]_v [[ negate f1]]_v = [[ FAnd f f1 ]]_(invert v)).
+ conclude
+ (min [[ negate f ]]_v [[ negate f1]]_v)
+ = (min [[ f ]]_(invert v) [[ negate f1]]_v) by H.
+ = (min [[ f ]]_(invert v) [[ f1]]_(invert v)) by H1.
+ done.
+ case FOr.
+ assume f : Formula.
+ by induction hypothesis we know
+ ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
+ assume f1 : Formula.
+ by induction hypothesis we know
+ ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1).
+ the thesis becomes
+ ([[ negate (FOr f f1) ]]_v=[[ FOr f f1 ]]_(invert v)).
+ the thesis becomes
+ (max [[ negate f ]]_v [[ negate f1]]_v = [[ FOr f f1 ]]_(invert v)).
+ conclude
+ (max [[ negate f ]]_v [[ negate f1]]_v)
+ = (max [[ f ]]_(invert v) [[ negate f1]]_v) by H.
+ = (max [[ f ]]_(invert v) [[ f1]]_(invert v)) by H1.
+ done.
+ case FImpl.
+ assume f : Formula.
+ by induction hypothesis we know
+ ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
+ assume f1 : Formula.
+ by induction hypothesis we know
+ ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1).
+ the thesis becomes
+ ([[ negate (FImpl f f1) ]]_v=[[ FImpl f f1 ]]_(invert v)).
+ the thesis becomes
+ (max (1 - [[ negate f ]]_v) [[ negate f1]]_v = [[ FImpl f f1 ]]_(invert v)).
+ conclude
+ (max (1 - [[ negate f ]]_v) [[ negate f1]]_v)
+ = (max (1 - [[ f ]]_(invert v)) [[ negate f1]]_v) by H.
+ = (max (1 - [[ f ]]_(invert v)) [[ f1]]_(invert v)) by H1.
+ done.
+ case FNot.
+ assume f : Formula.
+ by induction hypothesis we know
+ ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
+ the thesis becomes
+ ([[ negate (FNot f) ]]_v=[[ FNot f ]]_(invert v)).
+ the thesis becomes
+ (1 - [[ negate f ]]_v=[[ FNot f ]]_(invert v)).
+ conclude (1 - [[ negate f ]]_v) = (1 - [[f]]_(invert v)) by H.
+ done.
+qed.
+
+(*
+lemma negate_fun : ∀F,G. F ≡ G → negate F ≡ negate G.
+intros; intro v; rewrite > (negate_invert ? v);rewrite > (negate_invert ? v);
+apply H;
+qed.