Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Untitled

a guest Jul 8th, 2017 174 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  1. Require Import ZArith.
  2.  
  3. Module Type Zahl.
  4.   Parameter Zahl : Type.
  5.   Parameter plus : Zahl -> Zahl -> Zahl.
  6.   Parameter zerop : Zahl -> bool.
  7. End Zahl.
  8.  
  9. Module ZDirect <: Zahl.
  10.   Definition Zahl := Z.
  11.   Definition plus := Zplus.
  12.   Definition zerop := fun z => if Z_zerop z then true else false.
  13. End ZDirect.
  14.  
  15. Module ZQuotient <: Zahl.
  16.   Definition Zahl := (nat * nat)%type.
  17.   Definition plus x y :=
  18.     match x, y with (a,b),(c,d) =>
  19.       (a + c,b + d)
  20.     end.
  21.   Definition zerop x :=
  22.     match x with (a,b) =>
  23.       if eq_nat_dec a b
  24.         then true
  25.         else false
  26.     end.
  27. End ZQuotient.
  28.  
  29. Module MyModule (Integer : Zahl).
  30.   Import Integer.
  31.   Definition funky (a : Zahl) :=
  32.     if zerop (plus a a)
  33.       then a
  34.       else plus a (plus a a).
  35. End MyModule.
  36.  
  37. Module Z1 := MyModule ZDirect.
  38. Module Z2 := MyModule ZQuotient.
  39.  
  40. Check (Z1.funky).
  41.  
  42.  
  43. Axiom R : (nat*nat)%type -> (nat*nat)%type -> Prop.
  44. Axiom ZD_to_ZQ : Z -> (nat*nat)%type.
  45. Axiom ZQ_to_ZD : (nat*nat)%type -> Z.
  46. Axiom isomorphism1 : forall z,
  47.   ZQ_to_ZD (ZD_to_ZQ z) = z.
  48. Axiom isomorphism2 : forall z,
  49.   R (ZD_to_ZQ (ZQ_to_ZD z)) z.
  50. Axiom isomorphism_respectful : forall z z', R z z' -> ZQ_to_ZD z = ZQ_to_ZD z'.
  51.  
  52. Theorem funky_respectful : forall a b : (nat*nat)%type, R a b -> R (Z2.funky a) (Z2.funky b).
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top