Comment: int_1_summary
Integer inequalities, subtypes, and 
induction lemmas for subtypes.

Comment: int_1_intro
Definitions of inequality predicates on integers and
common integer subtypes. 

Also includes induction lemmas for naturals, and
experiment proving theorem with Ycombinator extract. 

Definition: is_int
is_int(x) ==  eval in isint(v)

Lemma: is_int_wf
[T:Type]. ∀[x:T]. (is_int(x) ∈ 𝔹supposing value-type(T) ∧ (T ⊆Base)

Lemma: assert-is_int
[T:Type]. ∀[x:T]. uiff(↑is_int(x);x ∈ ℤsupposing value-type(T) ∧ (T ⊆Base)

Definition: int?
int?(x) ==  eval in if is an integer then inl else inr 

Lemma: int?_wf
[T:Type]. ∀[x:T]. (int?(x) ∈ {y:ℤx}  T) supposing value-type(T) ∧ (T ⊆Base)

Comment: ge_gt_wf_com
These wf lemmas are used by EqCD
during rewriting to ensure that subterms 
come out in right order.

Lemma: comb_for_gt_wf
λi,j,z. (i > j) ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: comb_for_ge_wf
λi,j,z. (i ≥ ) ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: comb_for_le_wf
λi,j,z. (i ≤ j) ∈ ℤ ⟶ ℤ ⟶ (↓True) ⟶ ℙ

Definition: lele
i ≤ j ≤ ==  (i ≤ j) ∧ (j ≤ k)

Lemma: lelt_wf
[x,y,z:ℤ].  (x ≤ y < z ∈ ℙ)

Lemma: lele_wf
[x,y,z:ℤ].  (x ≤ y ≤ z ∈ ℙ)

Lemma: eq_int_eq_true_intro
[i,j:ℤ].  (i =z j) tt supposing j ∈ ℤ

Lemma: eq_int_eq_false_intro
[i,j:ℤ].  (i =z j) ff supposing ¬(i j ∈ ℤ)

Lemma: lt_int_eq_true_elim
[i,j:ℤ].  i < supposing i <tt

Lemma: lt_int_eq_false_elim
[i,j:ℤ].  ¬i < supposing i <ff

Lemma: eq_atom_eq_true_elim
[x,y:Atom].  y ∈ Atom supposing =a tt

Lemma: eq_atom_eq_false_elim
[x,y:Atom].  ¬(x y ∈ Atom) supposing =a ff

Lemma: int_seg_subtype
[m1,n1,m2,n2:ℤ].  {m1..n1-} ⊆{m2..n2-supposing (m2 ≤ m1) ∧ (n1 ≤ n2)

Lemma: int_seg_subtype_upper
[m1,n1,m2:ℤ].  {m1..n1-} ⊆{m2...} supposing m2 ≤ m1

Lemma: upper_subtype_upper
[m1,m2:ℤ].  {m1...} ⊆{m2...} supposing m2 ≤ m1

Lemma: upper_subtype_nat
[m:ℤ]. {m...} ⊆r ℕ supposing 0 ≤ m

Lemma: int_seg_subtype-nat
[m,n:ℤ].  {m..n-} ⊆r ℕ supposing 0 ≤ m

Lemma: subtype_rel-int_seg
[m1,n1,m2,n2:ℤ].  {m1..n1-} ⊆{m2..n2-supposing (m2 ≤ m1) ∧ (n1 ≤ n2)

Lemma: comb_for_int_seg_wf
λm,n,z. {m..n-} ∈ m:ℤ ⟶ n:ℤ ⟶ (↓True) ⟶ 𝕌1

Lemma: int_seg_properties
[i,j:ℤ]. ∀[y:{i..j-}].  i ≤ y < j

Lemma: decidable__equal_int_seg
i,j:ℤ. ∀x,y:{i..j-}.  Dec(x y ∈ {i..j-})

Definition: int_iseg
{i...j} ==  {k:ℤ(i ≤ k) ∧ (k ≤ j)} 

Lemma: int_iseg_wf
[i,j:ℤ].  ({i...j} ∈ Type)

Lemma: int_iseg_properties
[i,j:ℤ]. ∀[y:{i...j}].  ((i ≤ y) ∧ (y ≤ j))

Definition: increasing
increasing(f;k) ==  ∀i:ℕ1. i < (i 1)

Lemma: increasing_wf
[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  (increasing(f;k) ∈ ℙ)

Lemma: id_increasing
[k:ℕ]. increasing(λi.i;k)

Lemma: increasing_implies
[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  {∀[x,y:ℕk].  x < supposing x < y} supposing increasing(f;k)

Lemma: increasing_implies_le
[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  {∀[x,y:ℕk].  (f x) ≤ (f y) supposing x ≤ y} supposing increasing(f;k)

Lemma: increasing_le
[k,m:ℕ].  k ≤ supposing ∃f:ℕk ⟶ ℕm. increasing(f;k)

Lemma: increasing_is_id
[k:ℕ]. ∀[f:ℕk ⟶ ℕk].  ∀[i:ℕk]. ((f i) i ∈ ℤsupposing increasing(f;k)

Lemma: increasing_lower_bound
[k:ℕ]. ∀[f:ℕk ⟶ ℤ]. ∀[x:ℕk].  ((f 0) x) ≤ (f x) supposing increasing(f;k)

Lemma: int_lt_to_int_upper
i:ℤ. ∀[A:{i 1...} ⟶ ℙ]. ({∀j:ℤA[j] supposing i < j} ⇐⇒ {∀j:{i 1...}. A[j]})

Lemma: int_lt_to_int_upper_uniform
i:ℤ. ∀[A:{i 1...} ⟶ ℙ]. ({∀[j:ℤ]. A[j] supposing i < j} ⇐⇒ {∀[j:{i 1...}]. A[j]})

Lemma: int_le_to_int_upper
i:ℤ. ∀[A:{i...} ⟶ ℙ]. ({∀j:ℤA[j] supposing i ≤ j} ⇐⇒ {∀j:{i...}. A[j]})

Lemma: int_le_to_int_upper_uniform
i:ℤ. ∀[A:{i...} ⟶ ℙ]. ({∀[j:ℤ]. A[j] supposing i ≤ j} ⇐⇒ {∀[j:{i...}]. A[j]})

Comment: INT_INCLUSIONS_tcom
Inclusion relations between integer subypes

Lemma: nat_plus_inc
+ ⊆r ℕ

Lemma: nat_plus_inc_int_nzero
+ ⊆r ℤ-o

Comment: INDUCTION_tcom
Induction over naturals 

Use nat_ind_a or comp_nat_ind_a normally.
Use tactics when require no wf subgoals
  involving goal being proved. (e.g. when proving
  wf lemmas). 

Lemma: nat_ind
[P:ℕ ⟶ ℙ{k}]. (P[0]  (∀i:ℕ+(P[i 1]  P[i]))  {∀j:ℕP[j]})

Lemma: rec-nat-induction
[P:ℕ ⟶ ℙ]. (∀[n:ℕ]. (P[n]  P[n 1]))  (∀[n:ℕ]. P[n]) supposing Top ⊆P[0]

Lemma: complete_nat_ind
[P:ℕ ⟶ ℙ]. ((∀i:ℕ((∀j:ℕi. P[j])  P[i]))  (∀i:ℕP[i]))

Definition: suptype
suptype(S; T) ==  T ⊆ S

Definition: genrec
The general recursion operator.
The definition of genrec uses fix and is little bit
better than what AddRecDef would generate automatically 
(because AddRecDef leaves subterm of the form (\m. m) 
 which can be replaced by g)⋅

letrec rec(n)=g[n; rec] in rec  ==  fix((λrec,n. g[n; rec]))

Definition: genrec-ap
letrec rec(n)=g[n; rec] in rec(x) ==  fix((λrec,n. g[n; rec])) x

Lemma: complete_nat_measure_ind
[T:Type]. ∀[measure:T ⟶ ℕ]. ∀[P:T ⟶ ℙ].
  ((∀i:T. ((∀j:{j:T| measure[j] < measure[i]} P[j])  P[i]))  (∀i:T. P[i]))

Lemma: uniform_nat_measure_ind
[T:Type]. ∀[measure:T ⟶ ℕ]. ∀[P:T ⟶ ℙ].
  ((∀[i:T]. ((∀[j:{j:T| measure[j] < measure[i]} ]. P[j])  P[i]))  (∀[i:T]. P[i]))

Lemma: complete_nat_ind_with_y
[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ((∀j:ℕi. P[j])  P[i]))  (∀i:ℕP[i]))

Comment: natrec notes
The 'natrec' operator ⌜letrec f(n)=g[n;f] in
                        f⌝ is really just the general recursion operator
 ⌜letrec f(n)=g[n;f] in
   f ⌝,  but we "rename" it so that we can give wf lemma specific to the
 natural numbers.

 The definition of the genrec uses the combinator and is little bit
better than what AddRecDef would generate automatically (AddRecDef leaves
subterm of the form (\m. m) which can be replaced by g.⋅

Definition: natrec
The 'natrec' operator ⌜letrec f(n)=g[n;f] in
                        f⌝ is really just the general recursion operator
 ⌜letrec f(n)=g[n;f] in
   f ⌝
 but we "rename" it so that we can give wf lemma specific to the
 natural numbers.⋅

letrec f(n)=g[n; f] in ==  letrec f(n)=g[n; f] in 

Lemma: natrec_wf
[T:ℕ ⟶ Type]. ∀[g:n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]].  (letrec f(n)=g[n;f] in f ∈ n:ℕ ⟶ T[n])

Lemma: natrec_wf_intseg
[k:ℤ]. ∀[T:{k...} ⟶ Type]. ∀[g:n:{k...} ⟶ (m:{k..n-} ⟶ T[m]) ⟶ T[n]].  (letrec f(n)=g[n;f] in f ∈ n:{k...} ⟶ T[n])

Lemma: genrec-unroll
[g,n:Top].  (letrec f(n)=g[n;f] in f  g[n;letrec f(n)=g[n;f] in ])

Lemma: genrec-ap-unroll
[g,x:Top].  (letrec rec(n)=g[n;rec] in rec(x) g[x;λx.letrec rec(n)=g[n;rec] in rec(x)])

Lemma: natrec-unroll
[g,n:Top].  (letrec f(n)=g[n;f] in g[n;letrec f(n)=g[n;f] in f])

Lemma: complete-nat-induction
[P:ℕ ⟶ ℙ]. ((∀n:ℕ((∀m:ℕn. P[m])  P[n]))  (∀n:ℕP[n]))

Lemma: complete-nat-induction-ext
[P:ℕ ⟶ ℙ]. ((∀n:ℕ((∀m:ℕn. P[m])  P[n]))  (∀n:ℕP[n]))

Lemma: isint-int
[z:ℤ]. ∀[a,b:Top].  (if is an integer then else a)

Lemma: uniform-comp-nat-induction
[P:ℕ ⟶ ℙ]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m])  P[n]))  (∀[n:ℕ]. P[n]))

Lemma: uniform-comp-nat-induction-TYPE-tac
[P:ℕ ⟶ TYPE]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m])  P[n]))  (∀[n:ℕ]. P[n]))

Lemma: uniform-TI-less
[P:ℕ ⟶ ℙ]. uniform-TI(ℕ;x,y.y < x;x.P[x])

Lemma: assert_pushup_example
4 < 3 ∨ (3 ≤ 5)

Lemma: ite_rw_test
[n:ℕ]. ∀[i:ℕ+n].  False supposing (0 0 ∈ ℤ)) ∧ (n 0 ∈ ℤ))

Lemma: sqequal_n-wf
[x,y:Base]. ∀[n:ℕ].  (x ~n y ∈ Type)

Lemma: sqequal_n_wf
[x,y:Base]. ∀[n:ℕ].  (x ~n y ∈ Type)

Lemma: sq_stable__sqequal_n
[x,y:Base]. ∀[n:ℕ].  SqStable(x ~n y)

Lemma: sqle_n-wf
[x,y:Base]. ∀[n:ℕ].  (x ≤y ∈ Type)

Lemma: sqle_n_wf
[x,y:Base]. ∀[n:ℕ].  (x ≤y ∈ Type)

Lemma: sqle_n_subtype_rel
[a,b:Base]. ∀[n:ℕ].  a ≤supposing a ≤b

Lemma: sqequaln_sqlen
[a,b:Base]. ∀[n:ℕ].  (a ~n b) supposing ((a ≤b) and (b ≤a))

Lemma: sqlen_sqequaln
[a,b:Base]. ∀[n:ℕ].  a ≤supposing ~n b

Lemma: sqequaln_symm
[a,b:Base]. ∀[n:ℕ].  ~n supposing ~n a

Lemma: sqequal_n_add
x,y:Base. ∀n,m:ℕ.  ((x ~n y)  (x ~n y))

Definition: sqntype
sqntype(n;T) ==  ∀x,y:Base.  ((x y ∈ T)  (x ~n y))

Lemma: sqntype_wf
[T:Type]. ∀[n:ℕ].  (sqntype(n;T) ∈ ℙ)

Lemma: sq_stable__sqntype
[T:Type]. ∀[n:ℕ].  SqStable(sqntype(n;T))

Lemma: sqntype0
[T:Type]. sqntype(0;T)

Lemma: sqn+1type_dep_product
[T:Type]. ∀[S:T ⟶ Type]. ∀[n:ℕ].  (sqntype(n 1;t:T × S[t])) supposing ((∀t:T. sqntype(n;S[t])) and sqntype(n;T))

Lemma: sqn+1type_product
[T,S:Type]. ∀[n:ℕ].  (sqntype(n 1;T × S)) supposing (sqntype(n;S) and sqntype(n;T))

Lemma: sqntype_product
[T,S:Type]. ∀[n:ℕ].  (sqntype(n;T × S)) supposing (sqntype(n;S) and sqntype(n;T))

Lemma: sqntype_base
[n:ℕ]. sqntype(n;Base)

Lemma: sqntype_subtype
[A,B:Type]. ∀[n:ℕ].  (sqntype(n;A)) supposing (sqntype(n;B) and (A ⊆B))

Lemma: sqntype_subtype_base
[A:Type]. ∀[n:ℕ].  sqntype(n;A) supposing A ⊆Base

Lemma: sqntype_int
[n:ℕ]. sqntype(n;ℤ)

Lemma: sqntype_nat
[n:ℕ]. sqntype(n;ℕ)

Lemma: free-from-atom-nat
[a:Atom1]. ∀[n:ℕ].  a#n:ℕ

Lemma: free-from-atom2-nat
[a:Atom2]. ∀[n:ℕ].  a#n:ℕ

Lemma: free-from-atom-int
[a:Atom1]. ∀[n:ℤ].  a#n:ℤ

Lemma: free-from-atom2-int
[a:Atom2]. ∀[n:ℤ].  a#n:ℤ

Definition: abs-val
|x| ==  if x <then -x else fi 

Lemma: abs-val_wf
[x:ℤ]. (|x| ∈ ℕ)

Lemma: int_is_mono
[x:ℤ]. ∀[y:Base].  y ≤ supposing x ≤ y

Lemma: gcd-properties
  ((∃c:ℤ((c gcd(a;b)) a ∈ ℤ)) ∧ (∃d:ℤ((d gcd(a;b)) b ∈ ℤ)) ∧ (∃s,t:ℤ(gcd(a;b) ((s a) (t b)) ∈ ℤ)))

Lemma: better-gcd-properties
  ((∃c:ℤ((c better-gcd(a;b)) a ∈ ℤ))
  ∧ (∃d:ℤ((d better-gcd(a;b)) b ∈ ℤ))
  ∧ (∃s,t:ℤ(better-gcd(a;b) ((s a) (t b)) ∈ ℤ)))

Lemma: stamps-example
n:ℕ. ∃i:ℕ(∃j:ℕ [((n 8) ((3 i) (5 j)) ∈ ℤ)])

Lemma: stamps-example-ext
n:ℕ. ∃i:ℕ(∃j:ℕ [((n 8) ((3 i) (5 j)) ∈ ℤ)])

Definition: stamps35
stamps35(n) ==  TERMOF{stamps-example-ext:o, 1:l} n

Lemma: stamps35_wf
n:ℕ(stamps35(n) ∈ ∃i:ℕ(∃j:ℕ [((n 8) ((3 i) (5 j)) ∈ ℤ)]))

Lemma: absval_ifthenelse
[x:ℤ]. (|x| if 0 <then else -x fi )

Lemma: not-all-int_seg2
i,j:ℤ.  ∀[P,Q:{i..j-} ⟶ ℙ].  ((∀x:{i..j-}. (P[x] ∨ Q[x]))  (∀x:{i..j-}. P[x]))  (∃x:{i..j-}. Q[x]))

Lemma: not-all-int_seg
i,j:ℤ.  ∀[P:{i..j-} ⟶ ℙ]. ((∀x:{i..j-}. Dec(P[x]))  (∀x:{i..j-}. P[x]) ⇐⇒ ∃x:{i..j-}. P[x])))

Lemma: not-not-all-int_seg-xmiddle
a,b:ℤ. ∀P:{a..b-} ⟶ ℙ.  (¬¬(∀i:{a..b-}. (P[i] ∨ P[i]))))

Lemma: not-not-all-int_seg-shift
a,b:ℤ. ∀P:{a..b-} ⟶ ℙ.  ((∀i:{a..b-}. (¬¬P[i]))  (¬¬(∀i:{a..b-}. P[i])))

Definition: stable-union
stable-union(X;T;i,x.P[i; x]) ==  {x:X| ¬¬(∃i:T. P[i; x])} 

Lemma: stable-union_wf
[X,T:Type]. ∀[P:T ⟶ X ⟶ ℙ].  (stable-union(X;T;i,x.P[i;x]) ∈ Type)

Lemma: stable-union-decomp
[X,T:Type]. ∀[P:T ⟶ X ⟶ ℙ]. ∀[S:T ⟶ Type]. ∀[Q:i:T ⟶ S[i] ⟶ X ⟶ ℙ].
  stable-union(X;T;i,x.P[i;x]) ≡ stable-union(X;i:T × S[i];p,x.Q[fst(p);snd(p);x]) 
  supposing (∀x:X. ∀i:T. ∀s:S[i].  (Q[i;s;x]  (¬¬P[i;x]))) ∧ (∀x:X. ∀i:T.  (P[i;x]  (¬¬(∃s:S[i]. Q[i;s;x]))))

Home Index