Changeset 1928 for src/ASM/Util.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1908 r1928  
    795795qed.
    796796
     797lemma lt_m_n_to_exists_o_plus_m_n:
     798  ∀m, n: nat.
     799    m < n → ∃o: nat. m + o = n.
     800  #m #n
     801  cases m
     802  [1:
     803    #irrelevant
     804    %{n} %
     805  |2:
     806    #m' #lt_hyp
     807    %{(n - S m')}
     808    >commutative_plus in ⊢ (??%?);
     809    <plus_minus_m_m
     810    [1:
     811      %
     812    |2:
     813      @lt_S_to_lt
     814      assumption
     815    ]
     816  ]
     817qed.
     818
     819lemma lt_O_n_to_S_pred_n_n:
     820  ∀n: nat.
     821    0 < n → S (pred n) = n.
     822  #n
     823  cases n
     824  [1:
     825    #absurd
     826    cases(lt_to_not_zero 0 0 absurd)
     827  |2:
     828    #n' #lt_hyp %
     829  ]
     830qed.
     831
     832lemma exists_plus_m_n_to_exists_Sn:
     833  ∀m, n: nat.
     834    m < n → ∃p: nat. S p = n.
     835  #m #n
     836  cases m
     837  [1:
     838    #lt_hyp %{(pred n)}
     839    @(lt_O_n_to_S_pred_n_n … lt_hyp)
     840  |2:
     841    #m' #lt_hyp %{(pred n)}
     842    @(lt_O_n_to_S_pred_n_n)
     843    @(transitive_le … (S m') …)
     844    [1:
     845      //
     846    |2:
     847      @lt_S_to_lt
     848      assumption
     849    ]
     850  ]
     851qed.
     852
     853lemma plus_right_monotone:
     854  ∀m, n, o: nat.
     855    m = n → m + o = n + o.
     856  #m #n #o #refl >refl %
     857qed.
     858
     859lemma plus_left_monotone:
     860  ∀m, n, o: nat.
     861    m = n → o + m = o + n.
     862  #m #n #o #refl destruct %
     863qed.
     864
     865lemma minus_plus_cancel:
     866  ∀m, n : nat.
     867  ∀proof: n ≤ m.
     868    (m - n) + n = m.
     869  #m #n #proof /2 by plus_minus/
     870qed.
     871
     872lemma lt_to_le_to_le:
     873  ∀n, m, p: nat.
     874    n < m → m ≤ p → n ≤ p.
     875  #n #m #p #H #H1
     876  elim H
     877  [1:
     878    @(transitive_le n m p) /2/
     879  |2:
     880    /2/
     881  ]
     882qed.
     883
     884lemma eqb_decidable:
     885  ∀l, r: nat.
     886    (eqb l r = true) ∨ (eqb l r = false).
     887  #l #r //
     888qed.
     889
     890lemma r_Sr_and_l_r_to_Sl_r:
     891  ∀r, l: nat.
     892    (∃r': nat. r = S r' ∧ l = r') → S l = r.
     893  #r #l #exists_hyp
     894  cases exists_hyp #r'
     895  #and_hyp cases and_hyp
     896  #left_hyp #right_hyp
     897  destruct %
     898qed.
     899
     900lemma eqb_Sn_to_exists_n':
     901  ∀m, n: nat.
     902    eqb (S m) n = true → ∃n': nat. n = S n'.
     903  #m #n
     904  cases n
     905  [1:
     906    normalize #absurd
     907    destruct(absurd)
     908  |2:
     909    #n' #_ %{n'} %
     910  ]
     911qed.
     912
     913lemma eqb_true_to_eqb_S_S_true:
     914  ∀m, n: nat.
     915    eqb m n = true → eqb (S m) (S n) = true.
     916  #m #n normalize #assm assumption
     917qed.
     918
     919lemma eqb_S_S_true_to_eqb_true:
     920  ∀m, n: nat.
     921    eqb (S m) (S n) = true → eqb m n = true.
     922  #m #n normalize #assm assumption
     923qed.
     924
     925lemma eqb_true_to_refl:
     926  ∀l, r: nat.
     927    eqb l r = true → l = r.
     928  #l
     929  elim l
     930  [1:
     931    #r cases r
     932    [1:
     933      #_ %
     934    |2:
     935      #l' normalize
     936      #absurd destruct(absurd)
     937    ]
     938  |2:
     939    #l' #inductive_hypothesis #r
     940    #eqb_refl @r_Sr_and_l_r_to_Sl_r
     941    %{(pred r)} @conj
     942    [1:
     943      cases (eqb_Sn_to_exists_n' … eqb_refl)
     944      #r' #S_assm >S_assm %
     945    |2:
     946      cases (eqb_Sn_to_exists_n' … eqb_refl)
     947      #r' #refl_assm destruct normalize
     948      @inductive_hypothesis
     949      normalize in eqb_refl; assumption
     950    ]
     951  ]
     952qed.
     953
     954lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
     955  ∀r, l: nat.
     956    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
     957  #r #l #disj_hyp
     958  cases disj_hyp
     959  [1:
     960    #r_O_refl destruct @nmk
     961    #absurd destruct(absurd)
     962  |2:
     963    #exists_hyp cases exists_hyp #r'
     964    #conj_hyp cases conj_hyp #left_conj #right_conj
     965    destruct @nmk #S_S_refl_hyp
     966    elim right_conj #hyp @hyp //
     967  ]
     968qed.
     969
     970lemma neq_l_r_to_neq_Sl_Sr:
     971  ∀l, r: nat.
     972    l ≠ r → S l ≠ S r.
     973  #l #r #l_neq_r_assm
     974  @nmk #Sl_Sr_assm cases l_neq_r_assm
     975  #assm @assm //
     976qed.
     977
     978lemma eqb_false_to_not_refl:
     979  ∀l, r: nat.
     980    eqb l r = false → l ≠ r.
     981  #l
     982  elim l
     983  [1:
     984    #r cases r
     985    [1:
     986      normalize #absurd destruct(absurd)
     987    |2:
     988      #r' #_ @nmk
     989      #absurd destruct(absurd)
     990    ]
     991  |2:
     992    #l' #inductive_hypothesis #r
     993    cases r
     994    [1:
     995      #eqb_false_assm
     996      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
     997      @or_introl %
     998    |2:
     999      #r' #eqb_false_assm
     1000      @neq_l_r_to_neq_Sl_Sr
     1001      @inductive_hypothesis
     1002      assumption
     1003    ]
     1004  ]
     1005qed.
     1006
     1007lemma le_to_lt_or_eq:
     1008  ∀m, n: nat.
     1009    m ≤ n → m = n ∨ m < n.
     1010  #m #n #le_hyp
     1011  cases le_hyp
     1012  [1:
     1013    @or_introl %
     1014  |2:
     1015    #m' #le_hyp'
     1016    @or_intror
     1017    normalize
     1018    @le_S_S assumption
     1019  ]
     1020qed.
     1021
     1022lemma le_neq_to_lt:
     1023  ∀m, n: nat.
     1024    m ≤ n → m ≠ n → m < n.
     1025  #m #n #le_hyp #neq_hyp
     1026  cases neq_hyp
     1027  #eq_absurd_hyp
     1028  generalize in match (le_to_lt_or_eq m n le_hyp);
     1029  #disj_assm cases disj_assm
     1030  [1:
     1031    #absurd cases (eq_absurd_hyp absurd)
     1032  |2:
     1033    #assm assumption
     1034  ]
     1035qed.
     1036
     1037inverter nat_jmdiscr for nat.
     1038
     1039lemma plus_lt_to_lt:
     1040  ∀m, n, o: nat.
     1041    m + n < o → m < o.
     1042  #m #n #o
     1043  elim n
     1044  [1:
     1045    <(plus_n_O m) in ⊢ (% → ?);
     1046    #assumption assumption
     1047  |2:
     1048    #n' #inductive_hypothesis
     1049    <(plus_n_Sm m n') in ⊢ (% → ?);
     1050    #assm @inductive_hypothesis
     1051    normalize in assm; normalize
     1052    /2 by lt_S_to_lt/
     1053  ]
     1054qed.
     1055
     1056include "arithmetics/div_and_mod.ma".
     1057
     1058lemma n_plus_1_n_to_False:
     1059  ∀n: nat.
     1060    n + 1 = n → False.
     1061  #n elim n
     1062  [1:
     1063    normalize #absurd destruct(absurd)
     1064  |2:
     1065    #n' #inductive_hypothesis normalize
     1066    #absurd @inductive_hypothesis /2/
     1067  ]
     1068qed.
     1069
     1070lemma one_two_times_n_to_False:
     1071  ∀n: nat.
     1072    1=2*n→False.
     1073  #n cases n
     1074  [1:
     1075    normalize #absurd destruct(absurd)
     1076  |2:
     1077    #n' normalize #absurd
     1078    lapply (injective_S … absurd) -absurd #absurd
     1079    /2/
     1080  ]
     1081qed.
     1082
     1083let rec odd_p
     1084  (n: nat)
     1085    on n ≝
     1086  match n with
     1087  [ O ⇒ False
     1088  | S n' ⇒ even_p n'
     1089  ]
     1090and even_p
     1091  (n: nat)
     1092    on n ≝
     1093  match n with
     1094  [ O ⇒ True
     1095  | S n' ⇒ odd_p n'
     1096  ].
     1097
     1098let rec n_even_p_to_n_plus_2_even_p
     1099  (n: nat)
     1100    on n: even_p n → even_p (n + 2) ≝
     1101  match n with
     1102  [ O ⇒ ?
     1103  | S n' ⇒ ?
     1104  ]
     1105and n_odd_p_to_n_plus_2_odd_p
     1106  (n: nat)
     1107    on n: odd_p n → odd_p (n + 2) ≝
     1108  match n with
     1109  [ O ⇒ ?
     1110  | S n' ⇒ ?
     1111  ].
     1112  [1,3:
     1113    normalize #assm assumption
     1114  |2:
     1115    normalize @n_odd_p_to_n_plus_2_odd_p
     1116  |4:
     1117    normalize @n_even_p_to_n_plus_2_even_p
     1118  ]
     1119qed.
     1120
     1121let rec two_times_n_even_p
     1122  (n: nat)
     1123    on n: even_p (2 * n) ≝
     1124  match n with
     1125  [ O ⇒ ?
     1126  | S n' ⇒ ?
     1127  ]
     1128and two_times_n_plus_one_odd_p
     1129  (n: nat)
     1130    on n: odd_p ((2 * n) + 1) ≝
     1131  match n with
     1132  [ O ⇒ ?
     1133  | S n' ⇒ ?
     1134  ].
     1135  [1,3:
     1136    normalize @I
     1137  |2:
     1138    normalize
     1139    >plus_n_Sm
     1140    <(associative_plus n' n' 1)
     1141    >(plus_n_O (n' + n'))
     1142    cut(n' + n' + 0 + 1 = 2 * n' + 1)
     1143    [1:
     1144      //
     1145    |2:
     1146      #refl_assm >refl_assm
     1147      @two_times_n_plus_one_odd_p     
     1148    ]
     1149  |4:
     1150    normalize
     1151    >plus_n_Sm
     1152    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
     1153    [1:
     1154      normalize /2/
     1155    |2:
     1156      #refl_assm >refl_assm
     1157      @n_even_p_to_n_plus_2_even_p
     1158      @two_times_n_even_p
     1159    ]
     1160  ]
     1161qed.
     1162
     1163include alias "basics/logic.ma".
     1164
     1165let rec even_p_to_not_odd_p
     1166  (n: nat)
     1167    on n: even_p n → ¬ odd_p n ≝
     1168  match n with
     1169  [ O ⇒ ?
     1170  | S n' ⇒ ?
     1171  ]
     1172and odd_p_to_not_even_p
     1173  (n: nat)
     1174    on n: odd_p n → ¬ even_p n ≝
     1175  match n with
     1176  [ O ⇒ ?
     1177  | S n' ⇒ ?
     1178  ].
     1179  [1:
     1180    normalize #_
     1181    @nmk #assm assumption
     1182  |3:
     1183    normalize #absurd
     1184    cases absurd
     1185  |2:
     1186    normalize
     1187    @odd_p_to_not_even_p
     1188  |4:
     1189    normalize
     1190    @even_p_to_not_odd_p
     1191  ]
     1192qed.
     1193
     1194lemma even_p_odd_p_cases:
     1195  ∀n: nat.
     1196    even_p n ∨ odd_p n.
     1197  #n elim n
     1198  [1:
     1199    normalize @or_introl @I
     1200  |2:
     1201    #n' #inductive_hypothesis
     1202    normalize
     1203    cases inductive_hypothesis
     1204    #assm
     1205    try (@or_introl assumption)
     1206    try (@or_intror assumption)
     1207  ]
     1208qed.
     1209
     1210lemma two_times_n_plus_one_refl_two_times_n_to_False:
     1211  ∀m, n: nat.
     1212    2 * m + 1 = 2 * n → False.
     1213  #m #n
     1214  #assm
     1215  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
     1216  [1:
     1217    >assm
     1218    @conj
     1219    @two_times_n_even_p
     1220  |2:
     1221    * #_ #absurd
     1222    cases (even_p_to_not_odd_p … absurd)
     1223    #assm @assm
     1224    @two_times_n_plus_one_odd_p
     1225  ]
     1226qed.
     1227
     1228lemma not_Some_neq_None_to_False:
     1229  ∀a: Type[0].
     1230  ∀e: a.
     1231    ¬ (Some a e ≠ None a) → False.
     1232  #a #e #absurd cases absurd -absurd
     1233  #absurd @absurd @nmk -absurd
     1234  #absurd destruct(absurd)
     1235qed.
     1236
     1237lemma not_None_to_Some:
     1238  ∀A: Type[0].
     1239  ∀o: option A.
     1240    o ≠ None A → ∃v: A. o = Some A v.
     1241  #A #o cases o
     1242  [1:
     1243    #absurd cases absurd #absurd' cases (absurd' (refl …))
     1244  |2:
     1245    #v' #ignore /2/
     1246  ]
     1247qed.
     1248
    7971249lemma inclusive_disjunction_true:
    7981250  ∀b, c: bool.
     
    8341286qed.
    8351287
     1288(* XXX: to be moved into logic/basics.ma *)
     1289lemma and_intro_right:
     1290  ∀a, b: Prop.
     1291    a → (a → b) → a ∧ b.
     1292  #a #b /3/
     1293qed.
     1294
    8361295definition bool_to_Prop ≝
    8371296 λb. match b with [ true ⇒ True | false ⇒ False ].
     
    9241383interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    9251384
     1385(* Also extracts an equality proof (useful when not using Russell). *)
     1386notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
     1387 with precedence 10
     1388for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
     1389        λ${ident E}.$s ] (refl ? $t) }.
     1390
     1391notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
     1392 with precedence 10
     1393for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
     1394        λ${ident E}.$s ] (refl ? $t) }.
     1395
     1396notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
     1397 with precedence 10
     1398for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     1399       match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
     1400        λ${ident E}.$s ] ] (refl ? $t) }.
     1401
     1402notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
     1403 with precedence 10
     1404for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     1405       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
     1406        λ${ident E}.$s ] ] (refl ? $t) }.
     1407
    9261408lemma length_append:
    9271409 ∀A.∀l1,l2:list A.
Note: See TracChangeset for help on using the changeset viewer.