14.7 Inheritance Mechanism -- Examples

• (f a) is ill-typed where f:(x:A)B and a:A'. If there is a path coercion between A' and A, (f a) is transformed into (f a') where a' is the result of the application of this path coercion to a.
  
  
  Coq < Variables C:nat->Set; D:nat->bool->Set; E:bool->Set.
  C is assumed
  D is assumed
  E is assumed
  
  Coq < Variable f : (n:nat)(C n) -> (D (S n) true).
  f is assumed
  
  Coq < Coercion f : C >-> D.
  f is now a coercion
  
  Coq < Variable g : (n:nat)(b:bool)(D n b) -> (E b).
  g is assumed
  
  Coq < Coercion g : D >-> E.
  g is now a coercion
  
  Coq < Variable c : (C O).
  c is assumed
  
  Coq < Variable T : (E true) -> nat.
  T is assumed
  
  Coq < Check (T c).
  (T c)
       : nat
  
  We give now an example using identity coercions.
  
  
  Coq < Definition D' := [b:bool](D (S O) b).
  D' is defined
  
  Coq < Identity Coercion IdD'D : D' >-> D.
  IdD'D is now a coercion
  
  Coq < Print IdD'D.
  IdD'D = [b:bool][x:(D' b)]x
       : (b:bool)(D' b)->(D (S O) b)
  
  Coq < Variable d' : (D' true).
  d' is assumed
  
  Coq < Check (T d').
  (T d')
       : nat
  
  
  
  In the case of functional arguments, we use the monotonic rule of subtyping. Approximatively, to coerce t:(x:A)B towards (x:A')B', one have to coerce A' towards A and B towards B'. An example is given below:
  
  
  Coq < Variables A,B:Set; h:A->B.
  A is assumed
  B is assumed
  h is assumed
  
  Coq < Coercion h : A >-> B.
  h is now a coercion
  
  Coq < Variable U : (A -> (E true)) -> nat.
  U is assumed
  
  Coq < Variable t : B -> (C O).
  t is assumed
  
  Coq < Check (U t).
  (U [x:A](t x))
       : nat
  
  Remark the changes in the result following the modification of the previous example.
  
  
  Coq < Variable U' : ((C O) -> B) -> nat.
  U' is assumed
  
  Coq < Variable t' : (E true) -> A.
  t' is assumed
  
  Coq < Check (U' t').
  (U' [x:(C O)](t' x))
       : nat
  
• An assumption x:A when A is not a type, is ill-typed. It is replaced by x:A' where A' is the result of the application to A of the path coercion between the class of A and SORTCLASS if it exists. This case occurs in the abstraction [x:A]t, universal quantification (x:A)B, global variables and parameters of (co-)inductive definitions and functions. In (x:A)B, such a path coercion may be applied to B also if necessary.
  
  
  Coq < Variable Graph : Type.
  Graph is assumed
  
  Coq < Variable Node : Graph -> Type.
  Node is assumed
  
  Coq < Coercion Node : Graph >-> SORTCLASS.
  Node is now a coercion
  
  Coq < Variable G : Graph.
  G is assumed
  
  Coq < Variable Arrows : G -> G -> Type.
  Arrows is assumed
  
  Coq < Check Arrows.
  Arrows
       : (G)->(G)->Type
  
  Coq < Variable fg : G -> G.
  fg is assumed
  
  Coq < Check fg.
  fg
       : (G)->(G)
  
  
  
  
• (f a) is ill-typed because f:A is not a function. The term f is replaced by the term obtained by applying to f the path coercion between A and FUNCLASS if it exists.
  
  
  Coq < Variable bij : Set -> Set -> Set.
  bij is assumed
  
  Coq < Variable ap : (A,B:Set)(bij A B) -> A -> B.
  ap is assumed
  
  Coq < Coercion ap : bij >-> FUNCLASS.
  ap is now a coercion
  
  Coq < Variable b : (bij nat nat).
  b is assumed
  
  Coq < Check (b O).
  (ap nat nat b O)
       : nat
  
  Let us see the resulting graph of this session.
  
  
  Coq < Print Graph.
  [ap] : bij >-> FUNCLASS
  [Node] : Graph >-> SORTCLASS
  [h] : A >-> B
  [IdD'D; g] : D' >-> E
  [IdD'D] : D' >-> D
  [f; g] : C >-> E
  [g] : D >-> E
  [f] : C >-> D