CODEWITHSUNDEEP
coq
Tom And.
Tom And.

Reputation: 125

Coding ordered sets

As for having Coq programming experience, I'd like to know if there are any other ways to code, instead of my coding, preorder relations for using them in checking a function is non-decreasing. I replaced the datatypes and functions of my program to simple ones in the code below. mydata is a set with a preorder relation (i.e. with a reflexive and transitive relation) and is the range of the function mappingFunction which maps nat numbers to mydata. I couldn't define preorder relation on mydata when coding theorem mappingFunction_isIncreasing, so as a solution I mapped mydata to nat numbers through dataparts_toNat to enable me to define the preorder relation among them. I wonder if there is any other ways to do this program, for example without having dataparts_toNat. Thank you.

 (*defining the datatype*)
Inductive mydata : Set :=
  | part1 : mydata
  | part2 : mydata
  |part3 :mydata.

(* mapping to nats to have
        preorder relation(part1<part2<part3 and part1=part1 and part2=part2 and part3=part3)*)
Definition dataparts_toNat (n:mydata):nat :=
   match n with
          |part1 => 0
          |part2 => 1
          |part3 => 2
    end.

(* a sample function from nat to mydata which is always increasing or not changing*)
Definition mappingFunction
  (a1:nat): mydata :=
        match a1 with 
           |0=> part1
           |S(0) => part2
           |_ => part3
         end.    
Theorem mappingFunction_isIncreasing: forall(a1 a2: nat)(data1 data2: mydata),
   a1<=a2 -> (mappingFunction a1= data1 )/\(mappingFunction a2= 
data2) -> ((dataparts_toNat data1) <= dataparts_toNat(data2)).
Proof.

Upvotes: 0

Views: 103

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

(* The definition of mydata again, for completeness *)
Inductive mydata : Set :=
| part1 : mydata
| part2 : mydata
| part3 : mydata.

You can define a comparison as a boolean function mydata -> mydata -> bool:

Definition le_mydata_dec (d1 d2 : mydata) : bool :=
  match d1, d2 with
  | part1, _ => true
  | part2, (part2 | part3) => true
  | part3, part3 => true
  | _, _ => false
  end.

And from that, derive a comparison relation mydata -> mydata -> Prop (this is only one way, sometimes it's more convenient to define le_mydata as an Inductive proposition).

Definition le_mydata (d1 d2 : mydata) : Prop :=
  le_mydata_dec d1 d2 = true.

The mapping function is the same (renamed f for brevity):

(* a sample function from nat to mydata which is always increasing or not changing*)
Definition f
  (a1:nat): mydata :=
        match a1 with 
           |0=> part1
           |S(0) => part2
           |_ => part3
         end.

Now this is monotonicity:

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> le_mydata (f a1) (f a2).
Proof.
Abort.

You can use notations to replace le_mydata with a prettier <=. Here we are careful to not hide the preexisting notation <= for comparison of nat, by assigning this new notation to a new scope mydata_scope, delimited with the key mydata.

Infix "<=" := le_mydata : mydata_scope.
Delimit Scope mydata_scope with mydata.
(* now we can write  (x <= y)%mydata  instead of  le_mydata x y *)

The monotonicity theorem again, using that notation:

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> (f a1 <= f a2)%mydata.
Proof.
Abort.

Upvotes: 1

Related Questions