Library models

Module A1.

  CoInductive X := T | U | D.
  Notation "1" := U.
  Notation "2" := D.
  Definition mult x y :=
  match x,y with
  | 1,1 => 1
  | 2,2 => T
  | 2,_
  | _,2 => 2
  | _,_ => T
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 1,_ => y
  | _,1 => x
  | 2,2 => T
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: ~forall a b c, a^(b^c) = (a^b)^c.
  Proof. intro H; discriminate (H 1 2 2). Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A1.

Module A2.

  CoInductive X := T | U | D.
  Notation "1" := U.
  Notation "2" := D.
  Definition mult x y :=
  match x,y with
  | 1,1 => 1
  | 1,2
  | 2,1 => 2
  | _,_ => T
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,_ => x
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: ~forall a b, a^b = b^a.
  Proof. intro H. discriminate (H 1 2). Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A2.

Module A4.

  CoInductive X := T | U | D.
  Notation "1" := U.
  Notation "2" := D.
  Definition mult x y :=
  match x,y with
  | 1,1
  | 2,2 => 1
  | 2,_
  | _,2 => 2
  | _,_ => T
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 1,_ => y
  | _,1 => x
  | 2,2 => 1
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: ~forall a b c, a*(b*c) = (a*b)*c.
  Proof. intro H; discriminate (H T 2 2). Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A4.

Module A5.

  CoInductive X := T | U.
  Notation "1" := U.
  Definition mult (x y: X) :=
  match x,y with
  | _,_ => 1
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,T => T
  | _,_ => 1
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, T^a = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: ~forall a, a*1 = a.
  Proof. intro H. discriminate (H T). Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A5.

Module A6.

  CoInductive X := T | U.
  Notation "1" := U.
  Definition mult x y :=
  match x,y with
  | 1,1 => 1
  | _,_ => T
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,T => T
  | _,_ => 1
  end.
  Infix "^" := inter.
  Definition conv (x: X) := T.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, T^a = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: ~forall a, a``= a.
  Proof. intro H. discriminate (H 1). Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.
  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A6.

Module A7.

  CoInductive X := T | U | D | E.
  Notation "1" := U.
  Notation "2" := D.
  Notation "3" := E.
  Definition mult x y :=
  match x,y with
  | _,1 => x
  | 1,_ => y
  | _,_ => T
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 2,3
  | 3,2 => 2
  | 3,3 => T
  | _,_ => 1
  end.
  Infix "^" := inter.
  Definition conv x :=
  match x with
  | 3 => 2
  | 2 => 3
  | x => x
  end.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: ~forall a b, (a ^ b)`= a` ^ b`.
  Proof. intro H. discriminate (H 2 2). Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A7.

Module A8.

  CoInductive X := T | U | D.
  Notation "1" := U.
  Notation "2" := D.
  Definition mult x y :=
  match x,y with
  | _,T => T
  | _,1 => x
  | _,_ => 2
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | 1,_
  | _,1 => 1
  | T,T
  | 2,2 => T
  |_,_ => 2
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: ~forall a b, (a * b)`= b` * a`.
  Proof. intro H. discriminate (H T 2). Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A8.

Module A9.

  CoInductive X := T | U.
  Notation "1" := U.
  Definition mult x y :=
  match x,y with
  | 1,_ => y
  | _,1 => x
  | T,T => 1
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 1,1 => T
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 <> 1.
  Proof. discriminate. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A9.

Module A10.

  CoInductive X := T | U | D | E.
  Notation "1" := U.
  Notation "2" := D.
  Notation "3" := E.
  Definition mult x y :=
  match x,y with
  | 1,_ => y
  | _,1 => x
  | 3,3 => T
  | _,_ => 2
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 2,_ => 2
  | _,2 => 2
  | 3,3 => T
  | _,_ => 1
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: ~forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. intro H. discriminate (H 3 3). Qed.

End A10.

Module A11.

  CoInductive X := T | U.
  Notation "1" := U.
  Definition mult x y :=
  match x,y with
  | 1,_ => y
  | _,1 => x
  | T,T => 1
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 1,1 => 1
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: ~forall a, a*T = (1^(a*T))*T.
  Proof. intro H. discriminate (H T). Qed.
  Lemma mi1: forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. now destruct a; destruct b. Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A11.

Module A12.

  CoInductive X := T | U | D.
  Notation "1" := U.
  Notation "2" := D.
  Definition mult x y :=
  match x,y with
  | 1,_ => y
  | _,1 => x
  | T,T => T
  | 2,2 => T
  | _,_ => 2
  end.
  Infix "*" := mult.
  Definition inter x y :=
  match x,y with
  | T,_ => y
  | _,T => x
  | 1,1 => 1
  | 2,2 => 1
  | _,_ => 2
  end.
  Infix "^" := inter.
  Definition conv (x: X) := x.
  Notation "x `" := (conv x) (at level 20).

  Lemma iA: forall a b c, a^(b^c) = (a^b)^c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma iC: forall a b, a^b = b^a.
  Proof. now destruct a; destruct b. Qed.
  Lemma ixT: forall a, a^T = a.
  Proof. now destruct a. Qed.

  Lemma mA: forall a b c, a*(b*c) = (a*b)*c.
  Proof. now destruct a; destruct b; destruct c. Qed.
  Lemma mx1: forall a, a*1 = a.
  Proof. now destruct a. Qed.

  Lemma cI: forall a, a``= a.
  Proof. now destruct a. Qed.
  Lemma ci: forall a b, (a ^ b)`= a` ^ b`.
  Proof. now destruct a; destruct b. Qed.
  Lemma cm: forall a b, (a * b)`= b` * a`.
  Proof. now destruct a; destruct b. Qed.

  Lemma uu: 1 ^ 1 = 1.
  Proof. reflexivity. Qed.
  Lemma mT: forall a, a*T = (1^(a*T))*T.
  Proof. now destruct a. Qed.
  Lemma mi1: ~forall a b, (1^a)*b = ((1^a)*T)^b.
  Proof. intro H. discriminate (H 2 2). Qed.
  Lemma i1m: forall a b, 1^(a*b) = 1 ^ ((a ^ b`)*T).
  Proof. now destruct a; destruct b. Qed.

End A12.