fork download
copy 
  1. Require Import Orders.
  2. Require Import OrdersEx.
  3. Require Import MSets.
  4. Require Import Arith.
  5. Require Import Omega.
  6.  
  7. Module NatSet := Make Nat_as_OT.
  8.  
  9. Section MSet_set.
  10.  
  11.   Import NatSet.
  12.  
  13.   Definition has_upper_bound n
  14.     := For_all (gt n).
  15.  
  16.   Definition MFinNatSet (n:nat) : Type
  17.     := {s: t | has_upper_bound n s}.
  18.  
  19.   Definition MsingleS (n:nat) (i:nat): MFinNatSet n.
  20.   Proof.
  21.     unfold MFinNatSet.
  22.     case (lt_dec i n); intros H.
  23.     -
  24.       exists (singleton i).
  25.       unfold has_upper_bound, For_all.
  26.       intros x I.
  27.       apply singleton_spec in I.
  28.       omega.
  29.     -
  30.       exists empty.
  31.       unfold has_upper_bound, For_all.
  32.       intros x I.
  33.       apply empty_spec in I.
  34.       contradiction I.
  35.   Defined.
  36.  
  37.   Example MFoo: Empty (inter
  38.                          (proj1_sig (MsingleS 5 2))
  39.                          (proj1_sig (MsingleS 5 1))).
  40.   Proof.
  41.     simpl.
  42.     unfold Empty.
  43.     intros a.
  44.     intros H.
  45.     apply inter_spec in H.
  46.     destruct H as [H1 H2].
  47.     apply singleton_spec in H1.
  48.     apply singleton_spec in H2.
  49.     congruence.
  50.   Qed.
  51.  
  52. End MSet_set.
  53.  
Compilation error #stdin compilation error #stdout 0s 0KB
comments (?)
stdin
copy 
Standard input is empty
compilation info 
[1 of 1] Compiling Main             ( prog.hs, prog.o )

prog.hs:2:1: error:
    parse error (possibly incorrect indentation or mismatched brackets)
stdout
copy 
Standard output is empty
https://ideone.com/gKcl6j
language:
Haskell (ghc 8.4.4)
created:
7 years ago
visibility:
secret

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!