Commit 18cda710 authored by Joachim Bard's avatar Joachim Bard

adding union of intervals

parent 430414a8
......@@ -93,6 +93,24 @@ Proof.
- apply (Qle_antisym (ivhi iv1) (ivhi iv2)); auto.
Qed.
Definition unionIntv (iv1 iv2: intv) := mkIntv (Qmin (ivlo iv1) (ivlo iv2)) (Qmax (ivhi iv1) (ivhi iv2)).
Lemma subset_union_left iv1 iv2 : isSupersetIntv iv1 (unionIntv iv1 iv2) = true.
Proof.
destruct iv1, iv2. unfold unionIntv, isSupersetIntv; cbn.
apply Is_true_eq_true. apply andb_prop_intro. split.
- apply Is_true_eq_left. apply Qle_bool_iff. apply Q.le_min_l.
- apply Is_true_eq_left. apply Qle_bool_iff. apply Q.le_max_l.
Qed.
Lemma subset_union_right iv1 iv2 : isSupersetIntv iv2 (unionIntv iv1 iv2) = true.
Proof.
destruct iv1, iv2. unfold unionIntv, isSupersetIntv; cbn.
apply Is_true_eq_true. apply andb_prop_intro. split.
- apply Is_true_eq_left. apply Qle_bool_iff. apply Q.le_min_r.
- apply Is_true_eq_left. apply Qle_bool_iff. apply Q.le_max_r.
Qed.
(**
Definition of validity conditions for intv operations, Addition, Subtraction, Multiplication and Division
**)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment