matita/tests/compose.ma

   1
   2 include "logic/equality.ma".
   3
   4 theorem an_1:
   5 ∀ Univ:Set.
   6 ∀ a:Univ.
   7 ∀ is_a_theorem:Univ → Prop.
   8 ∀ not:Univ → Univ.
   9 ∀ or:Univ → Univ → Univ.
  10 ∀ H0:∀ U:Univ.∀ V:Univ.∀ X:Univ.∀ Y:Univ.∀ Z:Univ.
  11   is_a_theorem
  12     (or (not (or (not (or (not X) Y)) (or Z (or U V))))
  13         (or (not (or (not U) X)) (or Z (or V X)))).
  14 ∀ H1:∀ X:Univ.∀ Y:Univ.
  15   is_a_theorem (or (not X) Y) → is_a_theorem X → is_a_theorem Y.
  16 ∀ ABS:∀ X.is_a_theorem X.
  17 True.
  18 .
  19 intros 5.
  20 intros (H H1 ABS).
  21
  22 (* H1 o H *)
  23 compose (H) with (H1) (primo secondo).
  24 letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H ? ? ? ? ?));
  25 try assumption; [1,2: apply ABS]
  26 letin verifica_secondo ≝ (secondo ? ? ? ? ? ? ? = H1 ? ? (H ? ? ? ? ?) ?);
  27 try assumption; [1,2: apply ABS]
  28 clear verifica_primo verifica_secondo.
  29 compose (H) with (primo) (terzo).
  30 compose (H) with (secondo) (quarto).
  31 letin verifica_terzo_quarto ≝ (terzo ? ? ? ? ? = quarto ? ? ? ? ?);
  32 try assumption.
  33 clear verifica_terzo_quarto.
  34 clear primo secondo terzo quarto.
  35
  36 (* H1 o H1 *)
  37 compose (H1) with (H1) (primo secondo).
  38 letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H1 ? ? ? ?));
  39 try assumption; [1,2,3,4,5,6: apply ABS]
  40 letin verifica_secondo ≝ (secondo ? ? ? ? ? ? = H1 ? ? (H1 ? ? ? ?) ?);
  41 try assumption; [1,2,3,4,5,6: apply ABS]
  42 clear verifica_primo verifica_secondo.
  43 clear primo secondo.
  44
  45 (* close H1 o H1 with H *)
  46 compose H1 with H1 0.
  47 (*
  48 leaving the result under the sequent line and calling compose without
  49 the with parameter, will compose H with all the stuff under the sequent line
  50 *)
  51 compose 3 (H) (i1 i2 p1 p2 p3 p4 p5 p6 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12).
  52 exact I.
  53 qed.