Comment: well_fnd_summary
Well-founded predicate. Rank induction lemmas and

Comment: well_fnd_intro
Defines predicate saying that binary relation over some type
is well-founded.
Well-foundedness is phrased in terms of `course of values'
induction principle, since this is more useful constructively
than alternative formulations (e.g. saying that there are 
no infinite descending chains, or saying that every non-empty
subset has minimal element). NB: constructively, these 
alternative formulations are not equivalent.

Lemmas and tactics are introduced for induction on the rank of 
an expression (`inverse image induction'). One deficiency of Nuprl's
type theory is that in some situations (notably when proving well-formedness
goals) lemmas are unusable, and instead one must resort to using
tactics that reproduce equivalent sequences of primitive rules. 
The theorem `inv_image_ind_tp' provides template for such tactic
that mirrors the `inv_image_ind_a' lemma.

Definition: wellfounded
WellFnd{i}(A;x,y.R[x; y]) ==  ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (R[k; j]  P[k]))  P[j]))  {∀n:A. P[n]})

Lemma: wellfounded_wf
[A:Type]. ∀[r:A ⟶ A ⟶ ℙ].  (WellFnd{i}(A;x,y.r[x;y]) ∈ ℙ')

Lemma: wellfounded-irreflexive
[A:Type]. ∀[r:A ⟶ A ⟶ ℙ].  ∀a:A. r[a;a]) supposing WellFnd{i}(A;x,y.r[x;y])

Definition: uwellfounded
uWellFnd(A;x,y.R[x; y]) ==  ∀[P:A ⟶ ℙ]. ((∀[j:A]. ((∀[k:{k:A| R[k; j]} ]. P[k])  P[j]))  (∀[n:A]. P[n]))

Lemma: uwellfounded_wf
[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (uWellFnd(A;x,y.R[x;y]) ∈ ℙ')

Comment: INV_IMAGE_com
Inverse Image (Rank) Induction lemmas and tactics

inv_image_ind_a:   The basic lemma. Read this to understand proof method
inv_image_ind_tp:  template proof for the InvImageInd tactic
inv_image_ind_tac: Definition of the InvImageInd tactic
rank_ind_tac:      Definition of RankInd tactic.
                     Often more convenient than InvImageInd
inv_image_ind:     Test of InvImageInd tactic

Lemma: inv_image_ind_a
[T:Type]. ∀[r:T ⟶ T ⟶ ℙ]. ∀[S:Type].  ∀f:S ⟶ T. (WellFnd{i}(T;x,y.r[x;y])  WellFnd{i}(S;x,y.r[f x;f y]))

Lemma: inv_image_ind_tp
[T:Type]. ∀[r:T ⟶ T ⟶ ℙ]. ∀[S:Type].  ∀f:S ⟶ T. (WellFnd{i}(T;x,y.r[x;y])  WellFnd{i}(S;x,y.r[f x;f y]))

Lemma: inv_image_ind
[A:Type]. ∀[r:A ⟶ A ⟶ ℙ]. ∀[B:Type].  ∀f:B ⟶ A. (WellFnd{i}(A;x,y.r[x;y])  WellFnd{i}(B;x,y.r[f x;f y]))

Functionality lemmas for wellfounded predicate.
NB: wellfounded_functionality_wrt_implies_a assumes
subtype abstraction is proper predicate. ie. has wf thm. 

Lemma: comb_for_wellfounded_wf
λA,r,z. WellFnd{i}(A;x,y.r[x;y]) ∈ A:Type ⟶ r:(A ⟶ A ⟶ ℙ) ⟶ (↓True) ⟶ ℙ'

Lemma: wellfounded_functionality_wrt_implies
[T1,T2:Type]. ∀[r1:T1 ⟶ T1 ⟶ ℙ]. ∀[r2:T2 ⟶ T2 ⟶ ℙ].
  (∀x,y:T1.  {r1[x;y]  r2[x;y]})  {WellFnd{i}(T1;x,y.r1[x;y])  WellFnd{i}(T2;x,y.r2[x;y])} 
  supposing T1 T2 ∈ Type

Lemma: wellfounded_functionality_wrt_iff
[T1,T2:Type]. ∀[r1:T1 ⟶ T1 ⟶ ℙ]. ∀[r2:T2 ⟶ T2 ⟶ ℙ].
  (∀x,y:T1.  (r1[x;y] ⇐⇒ r2[x;y]))  (WellFnd{i}(T1;x,y.r1[x;y]) ⇐⇒ WellFnd{i}(T2;x,y.r2[x;y])) 
  supposing T1 T2 ∈ Type

Definition: pair-lex
pair-lex(A;Ra;Rb) ==  λx,y. ((Ra (fst(x)) (fst(y))) ∨ (((fst(x)) (fst(y)) ∈ A) ∧ (Rb (snd(x)) (snd(y)))))

Lemma: pair-lex_wf
[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].  (pair-lex(A;Ra;Rb) ∈ (A × B) ⟶ (A × B) ⟶ ℙ)

Lemma: product_well_fnd
[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
   WellFnd{i}(A × B;p1,p2.let a1,b1 p1 
                            in let a2,b2 p2 
                               in Ra[a1;a2] ∨ ((a1 a2 ∈ A) ∧ Rb[b1;b2])))

Lemma: pair-lex_well_fnd
[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
  (WellFnd{i}(A;a1,a2.Ra a1 a2)  WellFnd{i}(B;b1,b2.Rb b1 b2)  WellFnd{i}(A × B;p1,p2.pair-lex(A;Ra;Rb) p1 p2))

Home Index