lsp_impl_sr.v

rrika 2016-10-07 10:39:08.548846 UTC

(* my amateurish attempt at formalizing *)

Variable ooexpr   : Type.
Variable ootype   : Type.
Variable subtype  : ootype -> ootype -> Prop.
Variable isoftype : ooexpr -> ootype -> Prop.

Notation "a <: b" := (subtype a b) (at level 40).
Notation "a : b" := (isoftype a b) (at level 40).

Definition subtyping_transitive := forall {S T U: ootype}, S<:T -> T<:U -> S<:U.
Definition subsumption_rule := forall {S T: ootype} {s: ooexpr}, S<:T -> s:S -> s:T.

Definition liskov_substitution_principle :=
	forall (p: ooexpr -> Prop) {S T: ootype},
		let p' (V: ootype) := forall {v: ooexpr}, v : V -> p v
		in S <: T -> p' T -> p' S.

Theorem lsp_impl_sr : liskov_substitution_principle -> subsumption_rule.
  intro lsp.
  unfold liskov_substitution_principle in lsp.
  unfold subsumption_rule.
  intros.
  apply (lsp (fun x => x : T) S T); auto.
  Show Proof.
  (*
    fun (lsp : liskov_substitution_principle)
      (S T : ootype)
      (s : ooexpr)
      (H : S <: T)
      (H0 : s : S) =>
     lsp (fun x : ooexpr => x : T) S T H (fun (v : ooexpr) (H1 : v : T) => H1) s H0
  *)
Qed.