Pastebin launched a little side project called HostCabi.net, check it out ;-)Don't like ads? PRO users don't see any ads ;-)
Guest

Untitled

By: a guest on Nov 28th, 2012  |  syntax: None  |  size: 1.84 KB  |  hits: 12  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. Require Import Coq.Program.Program.
  2.  
  3. Inductive Bit: Set :=
  4.   | Zer: Bit
  5.   | One: Bit.
  6.  
  7. Inductive List (set1: Set): Set :=
  8.   | Empt: List set1
  9.   | Fill: set1 -> List set1 -> List set1.
  10.  
  11. Implicit Arguments Empt [[set1]].
  12.  
  13. Implicit Arguments Fill [[set1]].
  14.  
  15. Fixpoint meas {set1: Set} (list1: List set1): nat :=
  16.   match list1 with
  17.   | Empt => O
  18.   | Fill _ list2 => S (meas list2)
  19.   end.
  20.  
  21. Definition Nat: Set := List Bit.
  22.  
  23. Fixpoint Trim (nat1: Nat): Prop :=
  24.   match nat1 with
  25.   | Empt => True
  26.   | Fill Zer Empt => False
  27.   | Fill _ nat2 => Trim nat2
  28.   end.
  29.  
  30. Theorem VEGC: Trim (Fill Zer Empt) = False.
  31. Proof.
  32. trivial.
  33. Qed.
  34.  
  35. Theorem MCOW: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
  36. Proof.
  37. destruct bit1.
  38.   destruct nat1 as [ | bit2 nat2].
  39.     intro H1. rewrite VEGC in H1. contradiction.
  40.     trivial.
  41.   trivial.
  42. Qed.
  43.  
  44. Fixpoint Pos (nat1: Nat): Prop :=
  45.   match nat1 with
  46.   | Empt => False
  47.   | Fill Zer nat2 => Pos nat2
  48.   | Fill One _ => True
  49.   end.
  50.  
  51. Theorem NXJN: Pos Empt = False.
  52. Proof.
  53. trivial.
  54. Qed.
  55.  
  56. Theorem ZJSN: forall nat1: Nat, Pos (Fill Zer nat1) = Pos nat1.
  57. Proof.
  58. trivial.
  59. Qed.
  60.  
  61. Definition trim (nat1: Nat): Nat :=
  62.   match nat1 with
  63.   | Fill Zer Empt => Empt
  64.   | _ => nat1
  65.   end.
  66.  
  67. Program Fixpoint pred (nat1: Nat | Trim nat1 /\ Pos nat1) {measure (meas nat1)}: Nat :=
  68.   match nat1 with
  69.   | Empt => _
  70.   | Fill Zer nat3 => Fill One (pred nat3)
  71.   | Fill One nat3 => trim (Fill Zer nat3)
  72.   end.
  73.  
  74. Next Obligation.
  75. rewrite NXJN in p. contradiction.
  76. Qed.
  77.  
  78. Next Obligation.
  79. apply MCOW in t. rewrite ZJSN in p. split.
  80.   assumption.
  81.   assumption.
  82. Qed.
  83.  
  84. Theorem ZJBJ: forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1).
  85. Proof.
  86. destruct nat1 as [nat3 H1]. decompose [and] H1. induction nat3 as [ | bit1 nat4].
  87.   rewrite NXJN in H0. contradiction.
  88.   destruct bit1.