Pastebin launched a little side project called VERYVIRAL.com, check it out ;-) Want more features on Pastebin? Sign Up, it's FREE!
Guest

Untitled

By: a guest on Nov 29th, 2012  |  syntax: None  |  size: 1.47 KB  |  views: 8  |  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. Inductive Bit: Set :=
  2.   | Zer: Bit
  3.   | One: Bit.
  4.  
  5. Inductive List (set1: Set): Set :=
  6.   | Empt: List set1
  7.   | Fill: set1 -> List set1 -> List set1.
  8.  
  9. Implicit Arguments Empt [[set1]].
  10. Implicit Arguments Fill [[set1]].
  11.  
  12. Definition Nat: Set := List Bit.
  13.  
  14. Fixpoint Trim (nat1: Nat): Prop :=
  15.   match nat1 with
  16.   | Empt => True
  17.   | Fill Zer Empt => False
  18.   | Fill _ nat2 => Trim nat2
  19.   end.
  20.  
  21. Theorem KQQP: Trim (Fill Zer Empt) = False.
  22. Proof.
  23. trivial.
  24. Qed.
  25.  
  26. Theorem SLOF: forall nat1: Nat, Trim (Fill One nat1) = Trim nat1.
  27. Proof.
  28. trivial.
  29. Qed.
  30.  
  31. Theorem GLBR: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
  32. Proof.
  33. intros bit1 nat1 H1. destruct bit1.
  34.   destruct nat1 as [ | bit2 nat2].
  35.     rewrite KQQP in H1. contradiction.
  36.     trivial.
  37.   trivial.
  38. Qed.
  39.  
  40. Definition trim (nat1: Nat): Nat :=
  41.   match nat1 with
  42.   | Fill Zer Empt => Empt
  43.   | _ => nat1
  44.   end.
  45.  
  46. Fixpoint pred (nat1: Nat): Nat :=
  47.   match nat1 with
  48.   | Empt => Empt
  49.   | Fill Zer nat2 => Fill One (pred nat2)
  50.   | Fill One nat2 => trim (Fill Zer nat2)
  51.   end.
  52.  
  53. Theorem IEBL: forall nat1: Nat, pred (Fill Zer nat1) = Fill One (pred nat1).
  54. Proof.
  55. trivial.
  56. Qed.
  57.  
  58. Theorem ZFAF: forall nat1: Nat, Trim nat1 -> Trim (pred nat1).
  59. Proof.
  60. intros nat1 H1. induction nat1 as [ | bit1 nat2 IHnat2].
  61.   trivial.
  62.   destruct bit1.
  63.     apply GLBR in H1. specialize (IHnat2 H1). rewrite IEBL. rewrite SLOF. assumption.
  64.     destruct nat2 as [ | bit2 nat3].
  65.       trivial.
  66.       trivial.
  67. Qed.