matita/matita/lib/reverse_complexity/basics.ma

   1 include "basics/types.ma".
   2 include "arithmetics/nat.ma".
   3
   4 (********************************** pairing ***********************************)
   5 axiom pair: nat → nat → nat.
   6 axiom fst : nat → nat.
   7 axiom snd : nat → nat.
   8
   9 interpretation "abstract pair" 'pair f g = (pair f g).
  10
  11 axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
  12 axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
  13 axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉.
  14
  15 axiom le_fst : ∀p. fst p ≤ p.
  16 axiom le_snd : ∀p. snd p ≤ p.
  17 axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
  18
  19 lemma expand_pair: ∀x. x = 〈fst x, snd x〉.
  20 #x lapply (surj_pair x) * #a * #b #Hx >Hx >fst_pair >snd_pair //
  21 qed.
  22
  23 (************************************* U **************************************)
  24 axiom U: nat → nat →nat → option nat.
  25
  26 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
  27   U i x n = Some ? y → U i x m = Some ? y.
  28
  29 lemma unique_U: ∀i,x,n,m,yn,ym.
  30   U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
  31 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
  32   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
  33   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
  34    >Hn #HS destruct (HS) //
  35   ]
  36 qed.
  37
  38 definition code_for ≝ λf,i.∀x.
  39   ∃n.∀m. n ≤ m → U i x m = f x.
  40
  41 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
  42
  43 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
  44
  45 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
  46 #i #x #n normalize cases (U i x n)
  47   [%2 % * #y #H destruct|#y %1 %{y} //]
  48 qed.
  49
  50 lemma monotonic_terminate: ∀i,x,n,m.
  51   n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
  52 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
  53 qed.
  54
  55 definition termb ≝ λi,x,t.
  56   match U i x t with [None ⇒ false |Some y ⇒ true].
  57
  58 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
  59 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
  60 qed.
  61
  62 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
  63 #i #x #t * #y #H normalize >H //
  64 qed.
  65
  66 definition out ≝ λi,x,r.
  67   match U i x r with [ None ⇒ 0 | Some z ⇒ z].
  68
  69 definition bool_to_nat: bool → nat ≝
  70   λb. match b with [true ⇒ 1 | false ⇒ 0].
  71
  72 coercion bool_to_nat.
  73
  74 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
  75
  76 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
  77 #i #x #r #y % normalize
  78   [cases (U i x r) normalize
  79     [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
  80      #H1 destruct
  81     |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
  82      #H1 //
  83     ]
  84   |#H >H //]
  85 qed.
  86
  87 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
  88 #i #x #r % normalize
  89   [cases (U i x r) normalize //
  90    #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
  91    #H1 destruct
  92   |#H >H //]
  93 qed.
  94
  95 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
  96 #i #x #r normalize cases (U i x r) normalize >fst_pair //
  97 qed.
  98
  99 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
 100 #i #x #r normalize cases (U i x r) normalize >snd_pair //
 101 qed.
 102
 103
 104 definition total ≝ λf.λx:nat. Some nat (f x).
 105
 106