Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: f68e3c2784
Fetching contributors…

Cannot retrieve contributors at this time

file 445 lines (356 sloc) 12.903 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
Inductive True : Prop
Constructor I: True

Inductive False : Prop

Inductive Not (P: Prop) : Prop
Constructor Contradiction {P}: (P -> False) -> Not P

Inductive And (A B: Prop) : Prop
Constructor conj {A} {B}: A -> B -> And A B

Inductive Or (A B: Prop) : Prop
Constructor left {A} {B}: A -> Or A B
Constructor right {A} {B}: B -> Or A B

Inductive eq {A: Type} (a: A): A -> Prop
Constructor eq_refl {A} (a: A): eq a a

Definition eq_symm {A} (x y: A) (Hxy: eq x y) : eq y x :=
   match Hxy with
| eq_refl {A} x := eq_refl x
end

Definition eq_trans {A} (x y z: A) (Hxy: eq x y) (Hyz: eq y z) : eq x z :=
   match Hxy with
| eq_refl {A} xy :=
          match Hyz with
| eq_refl {A} yz := eq_refl _
          end
end


Definition Relation (A: Set) : Type := A -> A -> Prop

Inductive ReflexiveRel : Set
Constructor build_ReflexiveRel: (A: Set) -> (rel: Relation A) -> (refl: (x: A) -> rel x x) -> ReflexiveRel

Definition ReflexiveRel_t {rel: ReflexiveRel} : Set :=
   match rel with | build_ReflexiveRel A _ _ := A end

Definition ReflexiveRel_rel {rel: ReflexiveRel} : ReflexiveRel_t {rel} -> ReflexiveRel_t {rel} -> Prop:=
   match rel with
| build_ReflexiveRel _ rel _ := rel
   end

Definition ReflexiveRel_refl {rel: ReflexiveRel} : (x: ReflexiveRel_t {rel}) -> ReflexiveRel_rel {rel} x x :=
   match rel with
| build_ReflexiveRel _ _ refl := refl
   end

Inductive Nat: Set
Constructor O: Nat
Constructor S: Nat -> Nat

Inductive Vector (A: Set): Nat -> Set
Constructor nil {A: Set}: Vector A O
Constructor cons {A: Set} {n}: A -> Vector A n -> Vector A (S n)

Signature map {A B: Set} {n}: (f: A -> B) -> Vector A n -> Vector B n

Definition map {A B: Set} {n} (f: A -> B) (v: Vector A n) : Vector B n :=
  match v with
| nil {A} := nil
     | cons {A} {n} hd tl := cons (f hd) (map f tl)
end

Signature plus: Nat -> Nat -> Nat

Definition plus (n m: Nat) : Nat :=
  match n with
| O := m
     | S n := S (plus n m)
  end

Signature append {A} {n1 n2} (v1: Vector A n1) (v2: Vector A n2): Vector A (plus n1 n2)

Definition append {A} {n1 n2} (v1: Vector A n1) (v2: Vector A n2): Vector A (plus n1 n2) :=
  match v1 with
| nil {A} := v2
     | cons {A} {n1} hd tl := cons hd (append tl v2)
end

Inductive bool: Set
Constructor true: bool
Constructor false: bool

Inductive Eq: Set -> Set
Constructor build_eq {A}: (eqb: A -> A -> bool) -> Eq A

Definition eqb {A: Set} {eqA: Eq A}: A -> A -> bool :=
  match eqA with
| build_eq {A} eqb := eqb
  end


Inductive pair: Set -> Set -> Set
Constructor prod {A B: Set} (a: A) (b: B): pair A B

Definition eqb_bool (b1 b2: bool) : bool :=
  match prod b1 b2 with
| prod {_} {_} true true := true
| prod {_} {_} false false := true
| prod {_} {_} true false := false
| prod {_} {_} false true := false
end

Compute eqb_bool true true
Compute eqb_bool true false
Compute eqb_bool false true
Compute eqb_bool false false

Signature iota : Nat -> (size: Nat) -> Vector Nat size
Definition iota (start size: Nat) :=
  match size with
| O := nil
     | S size := cons start (iota (S start) size)
  end

Signature mult : Nat -> Nat -> Nat
Definition mult (n m: Nat) :=
  match n with
| O := O
     | S n := plus m (mult n m)
  end

Signature exp : Nat -> Nat -> Nat
Definition exp (n m: Nat) :=
  match n with
| O := S O
     | S n := mult m (exp n m)
  end

Definition three : Nat := S (S (S O))
Definition two : Nat := S (S O)

Signature min: Nat -> Nat -> Nat
Definition min (x y: Nat) :=
  match x with
| O := O
     | S n := match y with
| O := x
| S m := min n m
              end
end

Compute mult three three
Compute min (S (exp two three)) (exp two three)

Compute let x := exp two three in min (S x) x

Definition and_comm {P Q} (H: And P Q) :=
  match H with
| conj {P} {Q} p q := conj q p
end

Inductive expr: Set -> Set
Constructor Cste {A: Set}: A -> expr A
Constructor App {A B: Set}: expr (A -> B) -> expr A -> expr B
Constructor Ifte {A: Set}: expr bool -> expr A -> expr A -> expr A

Signature expr_sem {A: Set}: expr A -> A
Definition expr_sem {A: Set} (e: expr A) :=
  match e with
| Cste {A} c := c
     | App {A} {B} f a := (expr_sem f) (expr_sem a)
     | Ifte {A} b e1 e2 :=
        match expr_sem b with
| true := expr_sem e1
          | false := expr_sem e2
        end
end

Inductive formula: Set
Constructor f_forall: {A: Set} -> (A -> formula) -> formula
Constructor f_exists: {A: Set} -> (A -> formula) -> formula
Constructor f_neg: formula -> formula
Constructor f_and: formula -> formula -> formula
Constructor f_or: formula -> formula -> formula
Constructor f_impl: formula -> formula -> formula
Constructor f_iff: formula -> formula -> formula
Constructor f_pred: bool -> formula

Inductive exists {A: Set} (P: A -> Prop): Prop
Constructor witness {A: Set} (a: A) P: P a -> exists P

Inductive Iff: Prop -> Prop -> Prop
Constructor iff {P Q}: (P -> Q) -> (Q -> P) -> Iff P Q

Signature formula_sem: formula -> Prop
Definition formula_sem (f: formula) :=
   match f with
| f_forall {A} f := (x: A) -> formula_sem (f x)
      | f_exists {A} f := exists (\ x -> formula_sem (f x))
      | f_neg f := Not (formula_sem f)
      | f_and f1 f2 := And (formula_sem f1) (formula_sem f2)
      | f_or f1 f2 := Or (formula_sem f1) (formula_sem f2)
      | f_impl f1 f2 := (formula_sem f1) -> (formula_sem f2)
      | f_iff f1 f2 := Iff (formula_sem f1) (formula_sem f2)
      | f_pred b := eq b true
end

Signature andb (b1 b2: bool): bool
Definition andb (b1 b2: bool) :=
   match b1 with
| false := false
| true := b2
   end

Signature orb (b1 b2: bool): bool
Definition orb (b1 b2: bool) :=
   match b1 with
| true := true
| false := b2
   end

Signature notb (b: bool): bool
Definition notb (b: bool) :=
   match b with
| true := false
| false := true
end

Signature implb (b1 b2: bool): bool
Definition implb (b1 b2: bool) :=
   match b1 with
| false := true
| true := b2
   end

Signature eq_implb_orb_notb (b1 b2: bool): eq (implb b1 b2) (orb (notb b1) b2)
Definition eq_implb_orb_notb (b1 b2: bool) :=
  match b1 with
| true := eq_refl b2
     | false := eq_refl true
end

Signature eq_implb_orb_notb2 (b1 b2: bool): eq (implb b1 b2) (orb (notb b1) b2)
Definition eq_implb_orb_notb2 (b1 b2: bool) :=
  match prod b1 b2 with
| prod {_} {_} true true := eq_refl true
| prod {_} {_} true false := eq_refl false
| prod {_} {_} false _ := eq_refl true
end

Definition eq_trans2 {A} (x y z: A) (Hxy: eq x y) (Hyz: eq y z) : eq x z :=
  match Hyz with
| eq_refl {_} _ := Hxy
  end

Signature congr: {A: Type} -> (x y: A) -> (P: A -> Type) -> (Hxy: eq x y) -> (H: P x) -> P y
Definition congr {A: Type} (x y: A) (P: A -> Type) (Hxy: eq x y) (H: P x) :=
  match Hxy with
| eq_refl {_} _ := H
  end

Signature leibniz: {A: Type} -> (x y: A) -> ((P: A -> Prop) -> P x -> P y) -> eq x y
Definition leibniz {A: Type} (x y: A) (H: (P: A -> Prop) -> P x -> P y) :=
  H (eq {A} x) (eq_refl _)

Signature nat_ind (P: Nat -> Prop) (n: Nat) (H0: P O) (H1: (n: Nat) -> P n -> P (S n)): P n
Definition nat_ind (P: Nat -> Prop) (n: Nat) (H0: P O) (H1: (n: Nat) -> P n -> P (S n)) :=
  match n with
| O := H0
     | S n := H1 n (nat_ind P n H0 H1)
  end

Definition eqS (x y: Nat) (Hxy: eq x y) : eq (S x) (S y) :=
  match Hxy with
| eq_refl {_} _ := eq_refl (S x)
  end

Signature plusxO: (n: Nat) -> eq (plus n O) n
Definition plusx0 (n: Nat) :=
  nat_ind (\ x -> eq (plus x O) x) n
          (eq_refl O)
          (\ n (Pn: eq (plus n O) n) -> eqS _ _ Pn)

Definition plusxS (x y: Nat) : eq (plus x (S y)) (S (plus x y)) :=
  nat_ind (\ x -> eq (plus x (S y)) (S (plus x y))) x
(eq_refl (S y))
          (\n (Pn: eq (plus n (S y)) (S (plus n y))) -> eqS _ _ Pn)

Definition plus_comm (x y: Nat) : eq (plus x y) (plus y x) :=
  nat_ind (\ x -> eq (plus x y) (plus y x)) x
(eq_symm _ _ (plusxO y))
          (\ n (Pn: eq (plus n y) (plus y n)) ->
match (plusxS y n) with
| eq_refl {_} v := match Pn with
| eq_refl {_} m := eq_refl (S (plus y n))

                   end
end
)


Signature Nat_inversion (n: Nat) (P: Prop) (H1: eq n O -> P) (H2: (x: Nat) -> eq n (S x) -> P): P
Definition Nat_inversion (n: Nat) (P: Prop) (H1: eq n O -> P) (H2: (x: Nat) -> eq n (S x) -> P) : P :=
   match n with
| O := H1 (eq_refl O)
      | S x := H2 x (eq_refl (S x))
   end

Signature even: Nat -> bool
Definition even (n: Nat) :=
  match n with
| O := true
| S O := false
| S (S n) := even n
end

Inductive Fin: Nat -> Set
Constructor f0 {n}: Fin (S n)
Constructor fS {n}: Fin n -> Fin (S n)

Signature index {A} {n} (i: Fin n) (v: Vector A n) : A
Definition index {A} {n} (i: Fin n) (v: Vector A n) :=
  match i with
| f0 {_} := match v with | cons {_} {_} hd _ := hd end
| fS {_} i := match v with | cons {_} {_} _ tl := index i tl end
end

Inductive plus_arg_type: Set
Constructor plus_arg_Nat: plus_arg_type

Signature plusres (A: plus_arg_type) (B: plus_arg_type) : Set
Definition plusres A B :=
  match A with
| plus_arg_Nat := match B with
| plus_arg_Nat := Nat
end
end

Signature plus_arg_type2type: plus_arg_type -> Set
Definition plus_arg_type2type A :=
  match A with
| plus_arg_Nat := Nat
  end

Signature Plus {A: plus_arg_type} {B: plus_arg_type} : (plus_arg_type2type A) -> (plus_arg_type2type B) -> plusres A B
Definition Plus {A} {B} :=
  match A with
| plus_arg_Nat :=
       match B with
| plus_arg_Nat := plus
       end
end


Inductive uniqNat : Nat -> Set
Constructor uniqnat {sz: Nat}: (n: Nat) -> {H: eq sz n} -> uniqNat sz

Definition zero_uniqnat : uniqNat (S O) := uniqnat (S O)
exact eq_refl _

Definition doudou := Plus O O
exact plus_arg_Nat
exact plus_arg_Nat

Inductive Pos: Set
Constructor xh: Pos
Constructor xo: Pos -> Pos
Constructor xi: Pos -> Pos

Signature PosPlusCarry : Pos -> Pos -> bool -> Pos
Definition PosPlusCarry (p1 p2: Pos) (carry: bool) : Pos :=
  match p1 with
| xh := match p2 with
| xh := (match carry with | true := xi | false := xo end) xh
              | xo p2 := (match carry with | true := xo (PosPlusCarry xh p2 false) | false := xi p2 end)
              | xi p2 := (match carry with | true := xi (PosPlusCarry xh p2 false) | false := xo (PosPlusCarry xh p2 false) end)
            end
| xo p1 := match p2 with
| xh := (match carry with | true := xo (PosPlusCarry p1 xh false) | false := xi p1 end)
                 | xo p2 := (match carry with | true := xi | false := xo end) (PosPlusCarry p1 p2 false)
                 | xi p2 := (match carry with | true := xo (PosPlusCarry p1 p2 true) | false := xi (PosPlusCarry p1 p2 false) end)
               end
| xi p1 := match p2 with
| xh := (match carry with | true := xi (PosPlusCarry p1 xh true) | false := xo (PosPlusCarry p1 xh false) end)
                 | xo p2 := (match carry with | true := xo (PosPlusCarry p1 p2 true) | false := xi (PosPlusCarry p1 p2 false) end)
                 | xi p2 := (match carry with | true := xi (PosPlusCarry p1 p2 true) | false := xo (PosPlusCarry p1 p2 true) end)
               end
end

Definition PosPlus (p1 p2: Pos) : Pos :=
  PosPlusCarry p1 p2 false

Signature PosMult: Pos -> Pos -> Pos
Definition PosMult (p1 p2: Pos) : Pos :=
  match p1 with
| xh := p2
    | xo p1 := xo (PosMult p1 p2)
    | xi p1 := PosPlus p2 (xo (PosMult p1 p2))
  end

Signature PosPower: Pos -> Pos -> Pos
Definition PosPower (x y: Pos) : Pos :=
  match y with
| xh := x
| xo y := PosPower (PosMult x x) y
| xi y := PosMult x (PosPower (PosMult x x) y)
  end

Signature PosEq: Pos -> Pos -> bool
Definition PosEq (x y: Pos) :=
  match prod x y with
| prod {_} {_} xh xh := true
| prod {_} {_} (xi x) (xi y) := PosEq x y
| prod {_} {_} (xo x) (xo y) := PosEq x y
| _ := false
end

Definition PosOne := xh
Definition PosTwo := xo xh
Definition PosThree := xi xh

Definition PosSix := PosPlus PosThree PosThree

Compute PosSix

Definition PosThirtySix := PosMult PosSix PosSix

Compute PosThirtySix

Compute PosMult PosThirtySix PosThirtySix

Compute PosPower PosTwo (PosMult PosSix PosTwo)

Compute PosEq (PosPlus PosTwo PosThree) (PosPlus PosThree PosTwo)

Compute PosEq (PosPlus PosTwo PosThree) (PosPlus PosTwo PosSix)

Inductive N: Set
Constructor N0: N
Constructor NPos: Pos -> N

Inductive Z: Set
Constructor Z0: Z
Constructor ZPos: Pos -> Z
Constructor ZNeg: Pos -> Z

Compute Contradiction

Signature left_neq_right: {A: Type} -> (a: A) -> Not (eq (left a) (right a))
Definition left_neq_right {A: Type} (a: A) :=
Contradiction (\ (P: eq (left a) (right a)) -> match P with end)
Something went wrong with that request. Please try again.