---

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

Comment: well_fnd_intro
Defines predicate saying that a binary relation over some type
is well-founded.
Well-foundedness is phrased in terms of a `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 a 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 a template for such a 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:  A 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]))

Comment: WFND_FUNCTIONALITY_tcom
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;a1,a2.Ra[a1;a2])
  ⇒ WellFnd{i}(B;b1,b2.Rb[b1;b2])
  ⇒ 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