---

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 v = x in isint(v)

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

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

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

Lemma: int?_wf
∀[T:Type]. ∀[x:T]. (int?(x) ∈ {y:ℤ| y ~ x}  + T) supposing value-type(T) ∧ (T ⊆r 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 ≥ j ) ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ ℙ

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

Definition: lele
i ≤ j ≤ k ==  (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 i = 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 < j supposing i <z j = tt

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

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

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

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

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

Lemma: upper_subtype_upper
∀[m1,m2:ℤ].  {m1...} ⊆r {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-} ⊆r {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:ℕk - 1. f i < f (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].  f x < f y 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 ≤ m 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 ⊆r 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 a little bit
better than what AddRecDef would generate automatically 
(because AddRecDef leaves a subterm of the form (\m. g 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 a wf lemma specific to the
 natural numbers.

 The definition of the genrec uses the Y combinator and is a little bit
better than what AddRecDef would generate automatically (AddRecDef leaves
a subterm of the form (\m. g 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 a wf lemma specific to the
 natural numbers.⋅

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

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  n ~ g[n;letrec f(n)=g[n;f] in f ])

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 f n ~ 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 z is an integer then a else b ~ 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 ≤n y ∈ Type)

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

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

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

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

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

Lemma: sqequal_n_add
∀x,y:Base. ∀n,m:ℕ.  ((x ~n + m 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 ⊆r B))

Lemma: sqntype_subtype_base
∀[A:Type]. ∀[n:ℕ].  sqntype(n;A) supposing A ⊆r 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 <z 0 then -x else x fi 

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

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

Lemma: gcd-properties
∀a,b:ℤ.
  ((∃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
∀a,b:ℤ.
  ((∃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 <z x then x 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