Quelle  repulsive.pvs

%
% Repulsivity for horizontal vectors
% This is a 2D theory. 
% 

repulsive : THEORY
BEGIN

  IMPORTING horizontal,
       predicate_coordination_2D,
     vectors@basis_2D

  s,v,vo,vi,
  nv,nw,nh   : VAR Vect2
  nvo,nvi : VAR Vect2
  eps   : VAR Sign
  cc   : VAR posreal
  pt,px : VAR posreal
  

  % Time of closest approach
  tca(s,v) : real =
    IF zero_vect2?(v) THEN 0
    ELSE horizontal_tca(s,v)
    ENDIF

  repulsive?(s,v)(nv) : bool =
   LET tau1 = tca(s,v),
       tau2 = tca(s,nv) IN
     (s*v < 0 AND
     (tau2 <= 0 OR
     norm(s+tau1*v) < norm(s+tau2*nv)))
     OR
     (s*v>=0 AND (v = zero IMPLIES s*nv>=0) AND (v/=zero IMPLIES s*nv>s*v))

  repulsive_simple: LEMMA
    repulsive?(s,v)(nv) IMPLIES
    (s*v<0 AND tca(s,v)>0 AND
    (FORALL (t:nnreal): norm(s+t*nv)>=norm(s+tca(s,v)*v)))
    OR
    (s*v>=0 AND
    (FORALL (t:nnreal): norm(s+t*nv)>=norm(s))) 

  repulsive_transitive: LEMMA
    repulsive?(s,v)(nv) AND
    repulsive?(s,nv)(nw) IMPLIES
    repulsive?(s,v)(nw)

  not_repulsive_sum_closed: LEMMA
    sum_closed_2D?(LAMBDA (s,v): LAMBDA (nv): s*v<0 AND NOT repulsive?(s,v)(nv))

  repulsive_criteria(s,v,eps)(nv): bool =
    s  /= zero AND
    nv /= zero AND
    eps*det(s,v) <= 0 AND
    eps*det(s,nv) < 0 AND
    ((s*v < 0 AND
    eps*det(nv,v) < 0)
    OR
    (s*v>=0 AND (v = zero IMPLIES s*nv>=0) 
            AND (v/= zero IMPLIES s*nv> s*v)
     AND eps*det(nv,v) <= 0))

  repulsive_criteria_scal_s: LEMMA
    repulsive_criteria(s,v,eps)(nv) IFF
    repulsive_criteria(cc*s,v,eps)(nv)

  repulsive_criteria_scal_nv: LEMMA
    (s*v<0 AND (repulsive_criteria(s,v,eps)(cc*nv) IFF
    repulsive_criteria(s,v,eps)(nv)))
    OR
    (s*v>=0 AND (repulsive_criteria(s,v,eps)(cc*nv) IFF
    repulsive_criteria(s,(1/cc)*v,eps)(nv)))

  wedge_containment: LEMMA
    FORALL (e,f,g,h:Nz_vect2):
    (e*h>=0 AND f*h>0 AND g*h>0) AND
    (NOT (det(e,g)>=0 AND det(f,g)>0)) AND
    (NOT (det(e,g)<=0 AND det(f,g)<0)) AND
    e*v>=0 AND f*v>0 IMPLIES g*v>0

  repulsive_criteria_transitive: LEMMA
    repulsive_criteria(s,v,eps)(nv) AND
    repulsive_criteria(s,nv,eps)(nw) IMPLIES
    repulsive_criteria(s,v,eps)(nw)

  repulsive_criteria_transitive_odd1: LEMMA
    s*v<0 AND (s+pt*nv)*nv<0 AND
    repulsive_criteria(s,v,eps)(nv) AND
    repulsive_criteria(s+pt*nv,nv,eps)(nw) IMPLIES
    repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)

  rep_crit_odd2_ax: LEMMA
    FORALL(sx,sy,vx,vy,nvx,nvy,nwx,nwy:real,pt,px:posreal,eps:Sign) :
      px>0 AND pt>0
      AND nvx*sx+nvy*sy+nvx*nvx*pt+nvy*nvy*pt>=0
      AND sx*vx+sy*vy<0 AND sx*vy*eps-sy*vx*eps<=0
      AND nvy*sx*eps-nvx*sy*eps<0
      AND nvx*vy*eps-nvy*vx*eps<0
      AND nvy*sx*eps-nvx*sy*eps<=0
      AND -1*(nwx*sy*eps)-nvy*nwx*eps*pt+nwy*sx*eps+nvx*nwy*eps*pt<0
      AND nwx*sx+nwy*sy+nvx*nwx*pt+nvy*nwy*pt>nvx*sx+nvy*sy+nvx*nvx*pt+nvy*nvy*pt
      AND nwx*vy*eps-nwy*vx*eps<0
      IMPLIES
      -1*(nvx*sy*eps*pt)-nwx*sy*eps*px+nvy*sx*eps*pt+nwy*sx*eps*px<0

  repulsive_criteria_transitive_odd2: LEMMA
    s*v<0 AND (s+pt*nv)*nv>=0  AND
    repulsive_criteria(s,v,eps)(nv) AND
    repulsive_criteria(s+pt*nv,nv,eps)(nw) AND eps*det(nw,v) < 0
    IMPLIES
    repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)

  repulsive_criteria_transitive_odd3: LEMMA
    s*v>=0 AND pt>=1 AND
    repulsive_criteria(s,v,eps)(nv) AND
    repulsive_criteria(s+pt*nv,nv,eps)(nw) IMPLIES
    repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)

  repulsive_criteria_sum_closed: LEMMA
    repulsive_criteria(s,v,eps)(nv) AND
    repulsive_criteria(s,v,eps)(nw) IMPLIES
    repulsive_criteria(s,v,eps)(nv+nw)

  repulsive_criteria_indep_of_length: LEMMA
    s*v < 0 IMPLIES
    FORALL (c:posreal):
    repulsive_criteria(s,v,eps)(nv) IFF
    repulsive_criteria(s,v,eps)(c*nv)

  repulsive_criteria_repulsive: LEMMA
    repulsive_criteria(s,v,eps)(nv)
    IMPLIES
    repulsive?(s,v)(nv)

  repulsive_criteria_repulsive2: LEMMA
    repulsive?(s,v)(nv)
    AND eps * det(s, v) <= 0 AND eps * det(s, nv) < 0 AND nv /= zero
    AND (s*v>=0 IMPLIES eps*det(nv,v)<=0)
    IMPLIES
    repulsive_criteria(s,v,eps)(nv)

  repulsive_criteria_symmetric: LEMMA
    repulsive_criteria(s,v,eps)(nv) IFF
    repulsive_criteria(-s,-v,eps)(-nv)

  repulsive_criteria_coordinately_repulsive: LEMMA
    repulsive_criteria(s,vo-vi,eps)(nvo-vi) AND
    repulsive_criteria(-s,vi-vo,eps)(nvi-vo)
    IMPLIES
    repulsive?(s,vo-vi)(nvo-nvi) 

  foo: LEMMA
    repulsive_criteria(s,vo-vi,eps)(nvo-vi) AND
    repulsive_criteria(-s,vi-vo,eps)(nvi-vo)
    IMPLIES
    repulsive?(s,vo-vi)(nvo-nvi) 

  repulsive_increases_dist: LEMMA
    repulsive?(s,v)(nv) IMPLIES
    (s*v<0 AND horizontal_tca(s,v)>0 AND v/=zero AND
      FORALL (nnt:nnreal): norm(s+nnt*nv)>norm(s+horizontal_tca(s,v)*v))
    OR
    (s*v>=0 AND v/=zero AND horizontal_tca(s,v)<=0 AND
      FORALL (pt:posreal): norm(s+pt*nv)>norm(s))
    OR
    (v=zero AND FORALL (nnt:nnreal): norm(s+nnt*nv)>=norm(s))

END repulsive