matita/matita/lib/pts_dummy_new/subterms.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "pts_dummy_new/subst.ma".
  13
  14 inductive subterm : T → T → Prop ≝
  15   | appl : ∀M,N. subterm M (App M N)
  16   | appr : ∀M,N. subterm N (App M N)
  17   | lambdal : ∀M,N. subterm M (Lambda M N)
  18   | lambdar : ∀M,N. subterm N (Lambda M N)
  19   | prodl : ∀M,N. subterm M (Prod M N)
  20   | prodr : ∀M,N. subterm N (Prod M N)
  21   | dl : ∀M,N. subterm M (D M N)
  22   | dr : ∀M,N. subterm N (D M N)
  23   | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P.
  24
  25 inverter subterm_myinv for subterm (?%).
  26
  27 lemma subapp: ∀S,M,N. subterm S (App M N) →
  28  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  29 #S #M #N #subH (@(subterm_myinv … subH))
  30   [#M1 #N1 #eqapp destruct /4/
  31   |#M1 #N1 #eqapp destruct /4/
  32   |3,4,5,6,7,8: #M1 #N1 #eqapp destruct
  33   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp
  34    (cases (H2 eqapp))
  35     [* [* /3/ | #subN1 %1 %2 /2/ ]
  36     |#subN1 %2 /2/
  37     ]
  38   ]
  39 qed.
  40
  41 lemma sublam: ∀S,M,N. subterm S (Lambda M N) →
  42  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  43 #S #M #N #subH (@(subterm_myinv … subH))
  44   [1,2,5,6,7,8: #M1 #N1 #eqH destruct
  45   |3,4:#M1 #N1 #eqH destruct /4/
  46   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
  47    (cases (H2 eqH))
  48     [* [* /3/ | #subN1 %1 %2 /2/ ]
  49     |#subN1 %2 /2/
  50     ]
  51   ]
  52 qed.
  53
  54 lemma subprod: ∀S,M,N. subterm S (Prod M N) →
  55  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  56 #S #M #N #subH (@(subterm_myinv … subH))
  57   [1,2,3,4,7,8: #M1 #N1 #eqH destruct
  58   |5,6:#M1 #N1 #eqH destruct /4/
  59   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
  60    (cases (H2 eqH))
  61     [* [* /3/ | #subN1 %1 %2 /2/ ]
  62     |#subN1 %2 /2/
  63     ]
  64   ]
  65 qed.
  66
  67 lemma subd: ∀S,M,N. subterm S (D M N) →
  68  S = M ∨ S = N ∨ subterm S M ∨ subterm S N.
  69 #S #M #N #subH (@(subterm_myinv … subH))
  70   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
  71   |7,8: #M1 #N1 #eqH destruct /4/
  72   |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH
  73     (cases (H eqH))
  74     [* [* /3/ | #subN1 %1 %2 /2/ ]
  75     |#subN1 %2 /2/
  76     ]
  77   ]
  78 qed.
  79
  80 lemma subsort: ∀S,n. ¬ subterm S (Sort n).
  81 #S #n % #subH (@(subterm_myinv … subH))
  82   [1,2,3,4,5,6,7,8: #M1 #N1 #eqH destruct
  83   |/2/
  84   ]
  85 qed.
  86
  87 lemma subrel: ∀S,n. ¬ subterm S (Rel n).
  88 #S #n % #subH (@(subterm_myinv … subH))
  89   [1,2,3,4,5,6,7,8: #M1 #N1 #eqH destruct
  90   |/2/
  91   ]
  92 qed.
  93
  94 theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) →
  95  ∀M. P M.
  96 #P #H #M (cut (P M ∧ (∀N. subterm N M → P N)))
  97   [2: * //]
  98 (elim M)
  99   [#n %
 100     [@H #N1 #subN1 @False_ind /2/
 101     |#N #subN1 @False_ind /2/
 102     ]
 103   |#n %
 104     [@H #N1 #subN1 @False_ind /2/
 105     |#N #subN1 @False_ind /2/
 106     ]
 107   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 108    (cut (∀N.subterm N (App M1 M2) → P N))
 109     [#N1 #subN1 (cases (subapp … subN1))
 110       [* [* // | @Hind1 ] | @Hind2 ]]
 111     #Hcut % /3/
 112   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 113    (cut (∀N.subterm N (Lambda M1 M2) → P N))
 114     [#N1 #subN1 (cases (sublam … subN1))
 115       [* [* // | @Hind1 ] | @Hind2 ]]
 116    #Hcut % /3/
 117   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 118    (cut (∀N.subterm N (Prod M1 M2) → P N))
 119     [#N1 #subN1 (cases (subprod … subN1))
 120       [* [* // | @Hind1 ] | @Hind2 ]]
 121    #Hcut % /3/
 122   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2
 123    (cut (∀N.subterm N (D M1 M2) → P N))
 124     [#N1 #subN1 (cases (subd … subN1))
 125       [* [* // | @Hind1 ] | @Hind2 ]]
 126    #Hcut % /3/
 127   ]
 128 qed.
 129
 130 let rec size M ≝
 131 match M with
 132   [Sort N ⇒ 1
 133   |Rel N ⇒ 1
 134   |App P Q ⇒ size P + size Q + 1
 135   |Lambda P Q ⇒ size P + size Q + 1
 136   |Prod P Q ⇒ size P + size Q + 1
 137   |D P Q ⇒ size P + size Q + 1
 138   ]
 139 .
 140
 141 (* axiom pos_size: ∀M. 1 ≤ size M. *)
 142
 143 theorem Telim_size: ∀P: T → Prop.
 144  (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M.
 145 #P #H #M (cut (∀p,N. size N = p → P N))
 146   [2: /2/]
 147 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) //
 148 qed.
 149
 150 (* size of subterms *)
 151
 152 lemma size_subterm : ∀N,M. subterm N M → size N < size M.
 153 #N #M #subH (elim subH) normalize //
 154 #M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
 155 qed.