Skip to content

Commit

Permalink
Test to see if usable as a replacement for prob
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist authored and proux01 committed Mar 6, 2023
1 parent 181e307 commit fe36f5a
Showing 1 changed file with 26 additions and 0 deletions.
26 changes: 26 additions & 0 deletions theories/itv.v
Original file line number Diff line number Diff line change
Expand Up @@ -880,3 +880,29 @@ Goal (x%:inum * y%:inum)%:i01 = x%:inum%:i01.
Abort.

End Test2.

Section Test2'.

Variable R : realDomainType.

Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
(1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01.

Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
Proof.
apply/val_inj => /=.
by rewrite subr0 mulr1 opprB addrCA subrr addr0.
Qed.

Reserved Notation "p .~" (format "p .~", at level 5).

Definition onem (p : R) : R := 1 - p.
Notation "p .~" := (onem p).

Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].

Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
(1 - (p%:inum.~ * q%:inum.~))%:i01.

End Test2'.

0 comments on commit fe36f5a

Please sign in to comment.